theorem Th130: :: ZFMISC_1:131

for X being set st not X is empty & X is trivial holds
ex x being object st X = {x}