let X, x be set ; :: thesis: ( X \ {x} = X iff not x in X )
( X \ {x} = X iff X misses {x} ) by XBOOLE_1:83;
hence ( X \ {x} = X iff not x in X ) by Lm6, Lm7; :: thesis: verum