theorem :: ZFMISC_1:52

for x being object
for X being set holds
( {x} misses X or {x} /\ X = {x} ) by Lm6, Lm8;