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