let x1 be object ; :: thesis: {x1,x1} = {x1}

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

let x be object ; :: thesis: ( x in {x1,x1} iff x in {x1} )
( x in {x1,x1} iff x = x1 ) by TARSKI:def 2;
hence ( x in {x1,x1} iff x in {x1} ) by TARSKI:def 1; :: thesis: verum

end;

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