let x1, x2 be object ; :: thesis: {x1,x2} = {x1} \/ {x2}

now :: thesis: for x being object holds
( x in {x1,x2} iff x in {x1} \/ {x2} )

let x be object ; :: thesis: ( x in {x1,x2} iff x in {x1} \/ {x2} )
( x in {x1,x2} iff ( x = x1 or x = x2 ) ) by TARSKI:def 2;
then ( x in {x1,x2} iff ( x in {x1} or x in {x2} ) ) by TARSKI:def 1;
hence ( x in {x1,x2} iff x in {x1} \/ {x2} ) by XBOOLE_0:def 3; :: thesis: verum

end;

hence {x1,x2} = {x1} \/ {x2} by TARSKI:2; :: thesis: verum