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