theorem :: ZFMISC_1:48

for x being object
for X being set st {x} misses X holds
not x in X by Lm5;