theorem :: TARSKI_0:2

for X, Y being set st ( for x being object holds
( x in X iff x in Y ) ) holds
X = Y ;