let X, Y, x be set ; ( 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 ) )
not ( ( x in X implies x in Y ) & ( x in Y implies x in X ) & not X @ x = Y @ x )
thus
not ( ( x in X implies x in Y ) & ( x in Y implies x in X ) & not X @ x = Y @ x )
verum