theorem :: ZFMISC_1:139

for X being set holds
( not X is trivial iff for x being object holds not X \ {x} is empty )