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;
hence contradiction by A1, Th10, ORDINAL1:5; :: thesis: verum