let X be set ; :: thesis: not X, bool X are_equipotent
given f being Function such that A1: ( f is one-to-one & dom f = X & rng f = bool X ) ; :: according to WELLORD2:def 4 :: thesis: contradiction
defpred S₁[ set ] means for Y being set st Y = f . $1 holds
not $1 in Y;
consider Z being set such that
A2: for a being set holds
( a in Z iff ( a in X & S₁[a] ) ) from XBOOLE_0:sch 1();
Z c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Z or a in X )
thus ( not a in Z or a in X ) by A2; :: thesis: verum

end;

then consider a being set such that
A3: ( a in X & Z = f . a ) by A1, FUNCT_1:def 5;
not a in Z by A2, A3;
then ex Y being set st
( Y = f . a & a in Y ) by A2, A3;
hence contradiction by A2, A3; :: thesis: verum