theorem :: ZFMISC_1:61

for x being object
for X being set holds
( {x} \ X = {} or {x} \ X = {x} ) by Lm9, Lm10;