let X, Y be set ; :: thesis: ( ( X,Y are_equipotent or card X = card Y ) implies ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) )
assume ( X,Y are_equipotent or card X = card Y ) ; :: thesis: ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) )
then ( X,Y are_equipotent & 0 <> 1 & {0 ,1},{0 ,1} are_equipotent ) by CARD_1:21;
then ( card (Funcs X,{0 ,1}) = card (Funcs Y,{0 ,1}) & card (Funcs X,{0 ,1}) = card (bool X) & card (Funcs Y,{0 ,1}) = card (bool Y) ) by FUNCT_5:67, FUNCT_5:72;
hence ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) by CARD_1:21; :: thesis: verum