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