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