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

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

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

end;

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