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