let X, Y, x be set ; :: thesis: ( X @ x = Y @ x iff ( x in X iff x in Y ) )

thus ( X @ x = Y @ x implies ( x in X iff x in Y ) ) :: thesis: not ( ( x in X implies x in Y ) & ( x in Y implies x in X ) & not X @ x = Y @ x )

thus ( X @ x = Y @ x implies ( x in X iff x in Y ) ) :: thesis: not ( ( x in X implies x in Y ) & ( x in Y implies x in X ) & not X @ x = Y @ x )

proof

thus
not ( ( x in X implies x in Y ) & ( x in Y implies x in X ) & not X @ x = Y @ x )
:: thesis: verum
assume A1:
X @ x = Y @ x
; :: thesis: ( x in X iff x in Y )

thus ( x in X implies x in Y ) :: thesis: ( x in Y implies x in X )

then Y @ x = 1. Z_2 by Def3;

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

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

proof

assume
x in Y
; :: thesis: x in X
assume
x in X
; :: thesis: x in Y

then X @ x = 1. Z_2 by Def3;

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

end;then X @ x = 1. Z_2 by Def3;

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

then Y @ x = 1. Z_2 by Def3;

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