let X, x, y be set ; :: thesis: ( X @ x = X @ y iff ( x in X iff y in X ) )
thus ( X @ x = X @ y implies ( x in X iff y in X ) ) :: thesis: not ( ( x in X implies y in X ) & ( y in X implies x in X ) & not X @ x = X @ y )

proof

assume A1: X @ x = X @ y ; :: thesis: ( x in X iff y in X )
thus ( x in X implies y in X ) :: thesis: ( y in X implies x in X )

proof

assume x in X ; :: thesis: y in X
then X @ x = 1. Z_2 by Def3;
hence y in X by A1, Def3; :: thesis: verum

end;

assume y in X ; :: thesis: x in X
then X @ y = 1. Z_2 by Def3;
hence x in X by A1, Def3; :: thesis: verum

end;

assume A2: ( x in X iff y in X ) ; :: thesis: X @ x = X @ y

per cases ( X @ x = 0. Z_2 or X @ x = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def 2;

suppose X @ x = 0. Z_2 ; :: thesis: X @ x = X @ y

hence X @ x = X @ y by A2, Def3; :: thesis: verum

end;

suppose X @ x = 1. Z_2 ; :: thesis: X @ x = X @ y

hence X @ x = X @ y by A2, Def3; :: thesis: verum

end;

end;