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