<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
environ
begin
 reserve x,y,z for set;

scheme drinker { P[set] }:
 ((for x holds contradiction) implies contradiction) implies
 ((for x st (P[x] implies contradiction) implies contradiction holds P[x])
  implies
 ((for x st (P[x] implies for y holds P[y]) holds contradiction) implies
  contradiction))
proof
 assume
H: (for x holds contradiction) implies contradiction;
 assume
H0: for x st (P[x] implies contradiction) implies contradiction holds P[x];
 assume
H1: for x st (P[x] implies for y holds P[y]) holds contradiction;
 for x holds contradiction
 proof
  let x;
A: (P[x] implies for y holds P[y]) implies contradiction by H1;
  P[x] implies for y holds P[y]
  proof
   assume P[x];
   let y;
A0: ((P[y] implies contradiction) implies contradiction) implies P[y] by H0;
   (P[y] implies contradiction) implies contradiction
   proof
    assume
H3:  P[y] implies contradiction;
A1: (P[y] implies for z holds P[z]) implies contradiction by H1;
    P[y] implies for z holds P[z]
    proof
     assume
H4:   P[y];
     let z;
A2:  ((P[z] implies contradiction) implies contradiction) implies P[z] by H0;
     (P[z] implies contradiction) implies contradiction
     proof
      assume P[z] implies contradiction;
      thus contradiction by H3,H4;
     end;
     hence P[z] by A2;
    end;
    hence contradiction by A1;
   end;
   hence P[y] by A0;
  end;
  hence contradiction by A;
 end;
 hence contradiction by H;
end;