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