let x, X be set ; :: thesis: ( x in X implies X /\ {x} = {x} )
assume x in X ; :: thesis: X /\ {x} = {x}
then {x} c= X by Lm1;
hence X /\ {x} = {x} by XBOOLE_1:28; :: thesis: verum