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 )

proof

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 )

proof

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;

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

end;

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

proof

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

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 = Y @ x

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

end;

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

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

end;

end;

end;