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

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

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

{x,x} = {x}
by ENUMSET1:29;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;y in {x,y} by TARSKI:def 2;

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

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