for X, Y being set holds
( X = Y iff for x being object holds X @ x = Y @ x )