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 )

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 A2:
( x in X iff y in X )
; :: thesis: X @ x = X @ y
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 )

then X @ y = 1. Z_2 by Def3;

hence x in X by A1, Def3; :: thesis: verum

end;thus ( x in X implies y in X ) :: thesis: ( y in X implies x in X )

proof

assume
y in X
; :: thesis: x in X
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;then X @ x = 1. Z_2 by Def3;

hence y in X by A1, Def3; :: thesis: verum

then X @ y = 1. Z_2 by Def3;

hence x in X by A1, Def3; :: thesis: verum