let X, Y be set ; :: thesis: ( Y in X implies not X c= Y )
assume A1: Y in X ; :: thesis: not X c= Y
assume X c= Y ; :: thesis: contradiction
then Y in Y by A1;
hence contradiction ; :: thesis: verum