thus ( X is trivial implies for x, y being Element of X holds x = y ) :: thesis: ( ( for x, y being Element of X holds x = y ) implies X is trivial )

proof

assume Z: X is trivial ; :: thesis: for x, y being Element of X holds x = y
let x, y be Element of X; :: thesis: x = y
( x in X & y in X ) by Def2;
hence x = y by Z, ZFMISC_1:def 10; :: thesis: verum

end;

assume Z: for x, y being Element of X holds x = y ; :: thesis: X is trivial
let x, y be set ; :: according to ZFMISC_1:def 10 :: thesis: ( not x in X or not y in X or x = y )
assume ( x in X & y in X ) ; :: thesis: x = y
then ( x is Element of X & y is Element of X ) by Def2;
hence x = y by Z; :: thesis: verum