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;