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

thus ( X = Y implies for x being object holds X @ x = Y @ x ) ; :: thesis: ( ( for x being object holds X @ x = Y @ x ) implies X = Y )

thus ( ( for x being object holds X @ x = Y @ x ) implies X = Y ) :: thesis: verum

thus ( X = Y implies for x being object holds X @ x = Y @ x ) ; :: thesis: ( ( for x being object holds X @ x = Y @ x ) implies X = Y )

thus ( ( for x being object holds X @ x = Y @ x ) implies X = Y ) :: thesis: verum

proof

assume A1:
for x being object holds X @ x = Y @ x
; :: thesis: X = Y

thus X c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= X

assume y in Y ; :: thesis: y in X

then Y @ y = 1. Z_2 by Def3;

then X @ y = 1. Z_2 by A1;

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

end;thus X c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in X )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in Y )

assume y in X ; :: thesis: y in Y

then X @ y = 1. Z_2 by Def3;

then Y @ y = 1. Z_2 by A1;

hence y in Y by Def3; :: thesis: verum

end;assume y in X ; :: thesis: y in Y

then X @ y = 1. Z_2 by Def3;

then Y @ y = 1. Z_2 by A1;

hence y in Y by Def3; :: thesis: verum

assume y in Y ; :: thesis: y in X

then Y @ y = 1. Z_2 by Def3;

then X @ y = 1. Z_2 by A1;

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