let X, Y be set ; :: thesis: ( card X in card Y implies Y \ X <> {} )
assume A1: ( card X in card Y & Y \ X = {} ) ; :: thesis: contradiction
then Y c= X by XBOOLE_1:37;
then card Y c= card X by CARD_1:27;
hence contradiction by A1, CARD_1:14; :: thesis: verum