let x, y be set ; :: thesis: ( x <> y implies {x,y} \ {y} = {x} )
assume x <> y ; :: thesis: {x,y} \ {y} = {x}
then ( not x in {y} & y in {y} & not y in {x} & x in {x} & {x,y} = {y,x} ) by TARSKI:def 1;
hence {x,y} \ {y} = {x} by Lm12; :: thesis: verum