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

proof

let x be set ; :: 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 set such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 3;
A5: {y} c= X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {y} or z in X )
assume z in {y} ; :: thesis: z in X
hence z in X by A1, A3, TARSKI:def 1; :: thesis: verum

end;

f . y = {y} by A1, A3;
hence x in bool X by A4, A5; :: thesis: verum

end;

not X, bool X are_equipotent by Th29;
then A6: card X <> card (bool X) by Th21;
f is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 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, Th26;
then card X c< card (bool X) by A6, XBOOLE_0:def 8;
hence card X in card (bool X) by ORDINAL1:11; :: thesis: verum