let X, Y be set ; :: thesis: ( X c< Y implies Y \ X <> {} )
assume A1: X c< Y ; :: thesis: Y \ X <> {}
assume Y \ X = {} ; :: thesis: contradiction
then Y c= X by Lm1;
hence contradiction by A1, Th60; :: thesis: verum