let X, Y be set ; :: thesis: ( card X in card Y implies Y \ X <> {} )
assume that
A1: card X in card Y and
A2: Y \ X = {} ; :: thesis: contradiction
Y c= X by A2, XBOOLE_1:37;
then card Y c= card X by CARD_1:11;
hence contradiction by A1, CARD_1:4; :: thesis: verum