let x, y be object ; :: thesis: ( x <> y implies {x} \+\ {y} = {x,y} )
assume A1: x <> y ; :: thesis: {x} \+\ {y} = {x,y}
for z being object holds
( z in {x} \+\ {y} iff ( z = x or z = y ) )

proof

let z be object ; :: thesis: ( z in {x} \+\ {y} iff ( z = x or z = y ) )
A2: ( z in {y} iff z = y ) by TARSKI:def 1;
( z in {x} iff z = x ) by TARSKI:def 1;
hence ( z in {x} \+\ {y} iff ( z = x or z = y ) ) by A1, A2, XBOOLE_0:1; :: thesis: verum

end;

hence {x} \+\ {y} = {x,y} by TARSKI:def 2; :: thesis: verum