let x, y be set ; :: thesis: ( {x} \ {y} = {x} iff x <> y )
( {x} \ {y} = {x} iff not x in {y} ) by Lm6, Lm7, XBOOLE_1:83;
hence ( {x} \ {y} = {x} iff x <> y ) by TARSKI:def 1; :: thesis: verum