let X, Y be set ; :: thesis: ( X c< Y implies ex x being set st
( x in Y & not x in X ) )
assume A1: X c< Y ; :: thesis: ex x being set st
( x in Y & not x in X )
then A2: not for x being set holds
( x in X iff x in Y ) by TARSKI:2;
X c= Y by A1, Def8;
hence ex x being set st
( x in Y & not x in X ) by A2, TARSKI:def 3; :: thesis: verum