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