let X be set ; :: thesis: ( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )
X, card X are_equipotent by CARD_1:def 5;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by WELLORD2:def 4;
deffunc H₁( set ) -> set = f .: $1;
consider g being Function such that
A4: ( dom g = bool X & ( for x being set st x in bool X holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();
thus bool X, bool (card X) are_equipotent :: thesis: card (bool X) = card (bool (card X))

proof

take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & proj1 g = bool X & proj2 g = bool (card X) )
thus g is one-to-one :: thesis: ( proj1 g = bool X & proj2 g = bool (card X) )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 g or not b₁ in proj1 g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume that
A5: x in dom g and
A6: y in dom g and
A7: g . x = g . y ; :: thesis: x = y
A8: ( g . x = f .: x & g . y = f .: y ) by A4, A5, A6;
A9: y c= x

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in y or z in x )
assume A10: z in y ; :: thesis: z in x
then f . z in f .: y by A2, A4, A6, FUNCT_1:def 12;
then ex u being set st
( u in dom f & u in x & f . z = f . u ) by A7, A8, FUNCT_1:def 12;
hence z in x by A1, A2, A4, A6, A10, FUNCT_1:def 8; :: thesis: verum

end;

x c= y

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in y )
assume A11: z in x ; :: thesis: z in y
then f . z in f .: x by A2, A4, A5, FUNCT_1:def 12;
then ex u being set st
( u in dom f & u in y & f . z = f . u ) by A7, A8, FUNCT_1:def 12;
hence z in y by A1, A2, A4, A5, A11, FUNCT_1:def 8; :: thesis: verum

end;

hence x = y by A9, XBOOLE_0:def 10; :: thesis: verum

end;

thus dom g = bool X by A4; :: thesis: proj2 g = bool (card X)
thus rng g c= bool (card X) :: according to XBOOLE_0:def 10 :: thesis: bool (card X) c= proj2 g

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in bool (card X) )
assume x in rng g ; :: thesis: x in bool (card X)
then consider y being set such that
A12: y in dom g and
A13: x = g . y by FUNCT_1:def 5;
A14: f .: y c= rng f by RELAT_1:144;
g . y = f .: y by A4, A12;
hence x in bool (card X) by A3, A13, A14; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool (card X) or x in proj2 g )
A15: f " x c= dom f by RELAT_1:167;
assume x in bool (card X) ; :: thesis: x in proj2 g
then f .: (f " x) = x by A3, FUNCT_1:147;
then g . (f " x) = x by A2, A4, A15;
hence x in proj2 g by A2, A4, A15, FUNCT_1:def 5; :: thesis: verum

end;

hence card (bool X) = card (bool (card X)) by CARD_1:21; :: thesis: verum