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: f is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A3: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
then ( f . x = {x} & f . y = {y} ) by A1;
hence x = y by A3, ZFMISC_1:6; :: thesis: verum

end;

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
A4: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
A5: f . y = {y} by A1, A4;
{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, A4, TARSKI:def 1; :: thesis: verum

end;

hence x in bool X by A4, A5; :: thesis: verum

end;

then A6: card X c= card (bool X) by A1, A2, Th26;
not X, bool X are_equipotent by Th29;
then card X <> card (bool X) by Th21;
then card X c< card (bool X) by A6, XBOOLE_0:def 8;
hence card X in card (bool X) by ORDINAL1:21; :: thesis: verum