let x be object ; :: thesis: for X being set holds
( X \ {x} = X iff not x in X )
let 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 Lm5, Lm6; :: thesis: verum