thus ( X = Y implies ( X c= Y & Y c= X ) ) ; :: thesis: ( X c= Y & Y c= X implies X = Y )
assume ( X c= Y & Y c= X ) ; :: thesis: X = Y
then for x being set holds
( x in X iff x in Y ) by TARSKI:def 3;
hence X = Y by TARSKI:2; :: thesis: verum