theorem :: ZFMISC_1:39

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