theorem :: ZFMISC_1:31

for x being object
for X being set holds
( {x} c= X iff x in X ) by Lm1;