theorem :: ZFMISC_1:58

for x being object
for X being set holds
( not X \ {x} = {} or X = {} or X = {x} )