let X, Y be set ; :: thesis: ( X = Y iff for x being set holds X @ x = Y @ x )
thus ( X = Y implies for x being set holds X @ x = Y @ x ) ; :: thesis: ( ( for x being set holds X @ x = Y @ x ) implies X = Y )
thus ( ( for x being set holds X @ x = Y @ x ) implies X = Y ) :: thesis: verum

proof

assume A1: for x being set holds X @ x = Y @ x ; :: thesis: X = Y
thus X c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in Y )
assume A2: y in X ; :: thesis: y in Y
X @ y = 1. Z_2 by A2, Def3;
then Y @ y = 1. Z_2 by A1;
hence y in Y by Def3; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in X )
assume A3: y in Y ; :: thesis: y in X
Y @ y = 1. Z_2 by A3, Def3;
then X @ y = 1. Z_2 by A1;
hence y in X by Def3; :: thesis: verum

end;