let X be set ; :: thesis: card X in card (bool X)
deffunc H₁( object ) -> set = {$1};
consider f being Function such that
A1: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
A2: rng f c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool X )
assume x in rng f ; :: thesis: x in bool X
then consider y being object such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 3;
A5: {y} c= X by A1, A3, TARSKI:def 1;
f . y = {y} by A1, A3;
hence x in bool X by A4, A5; :: thesis: verum

end;

A6: card X <> card (bool X) by Th4, Th12;
f is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A7: ( x in dom f & y in dom f ) and
A8: f . x = f . y ; :: thesis: x = y
( f . x = {x} & f . y = {y} ) by A1, A7;
hence x = y by A8, ZFMISC_1:3; :: thesis: verum

end;

then card X c= card (bool X) by A1, A2, Th9;
hence card X in card (bool X) by A6, ORDINAL1:11, XBOOLE_0:def 8; :: thesis: verum