environ
vocabularies PROPOSIT;
notations PROPOSIT;
constructors PROPOSIT;
begin
reserve x,y for set;
(p implies for x holds q) implies (p implies q);
(p implies q) implies (p implies for x holds q);
((ex x st p ) implies q ) implies (p implies q);
(p implies q) implies ((ex x st p ) implies q );
(for x holds p) implies p;
p implies (ex x st p);
(for x ex y st p) implies (ex y st for x holds p);
::> *4
(ex y st for x holds p) implies (for x ex y st p);
::> *4
(ex y st for x holds p) implies (for x ex y st p)
proof
assume (ex y st for x holds p);
then consider y such that y: for x holds p;
thus (for x ex y st p)
proof
let x;
take y;
thus p by y;
end;
end;
::> 4: This inference is not accepted