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