theorem :: ZFMISC_1:33

for x being object
for Y being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) ) by Lm3;