for x being object
for X being set st x in X holds
ex Y being set st
( Y in X & ( for x being object holds
( not x in X or not x in Y ) ) ) by TARSKI_0:5;