1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
horizon := 0;;
thm `;
assume ?x:A. T [1];
let P be A->bool;
thus ?x. P x ==> !y. P y
proof
(?x. ~P x) \/ ~(?x. ~P x); // LEM
cases by -; // \/E
suppose ?x. ~P x;
consider x such that
~P x [2] by -; // ?E
take x; // ?I
assume P x; // ==>I
F by 2,-; // ~E
qed by -; // FE
suppose ~(?x. ~P x) [3];
consider x such that
(\x:A. T) x by 1; // ?E
take x; // ?I
assume P x; // ==>I
let y be A; // !I
P y \/ ~P y; // LEM
cases by -; // \/E
suppose P y;
qed by -; //
suppose ~P y;
?y. ~P y
proof
take y; // ?I
qed by -; //
F by 3,-; // ~E
qed by -; // FE
end;
end`;;
|
