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

proof

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

end;

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