theorem :: ZFMISC_1:59

for x being object
for X being set holds
( {x} \ X = {x} iff not x in X ) by Lm5, Lm6, XBOOLE_1:83;