theorem :: ZFMISC_1:45

for x being object
for X being set st X /\ {x} = {x} holds
x in X by Lm7;