let X, W 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 by A1, A2;
then A3: card (bool X) c= card W by CARD_1:11;
A4: card X in card (bool X) by CARD_1:14;
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:5; :: thesis: verum