let x, y be object ; :: thesis: ( {x,y} is trivial iff x = y )

hereby :: thesis: ( x = y implies {x,y} is trivial )

A1: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence ( {x,y} is trivial implies x = y ) by A1; :: thesis: verum

end;

{x,x} = {x} by ENUMSET1:29;
hence ( x = y implies {x,y} is trivial ) ; :: thesis: verum