let W, X be set ; :: thesis: ( W is subset-closed & X in W implies ( not X,W are_equipotent & card X in card W ) )
assume A1: W is subset-closed ; :: thesis: ( not X in W or ( not X,W are_equipotent & card X in card W ) )
assume A2: X in W ; :: thesis: ( not X,W are_equipotent & card X in card W )
bool X c= W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in W )
assume x in bool X ; :: thesis: x in W
hence x in W by A1, A2, CLASSES1:def 1; :: thesis: verum

end;

then A3: card (bool X) c= card W by CARD_1:27;
A4: card X in card (bool X) by CARD_1:30;
then card X in card W by A3;
then card X <> card W ;
hence ( not X,W are_equipotent & card X in card W ) by A4, A3, CARD_1:21; :: thesis: verum