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 A1: X is trivial ; :: thesis: for x, y being Element of X holds x = y
let x, y be Element of X; :: thesis: x = y

per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: x = y

then ( x in X & y in X ) by Def1;
hence x = y by A1; :: thesis: verum

end;

suppose X is empty ; :: thesis: x = y

then ( x = {} & y = {} ) by Def1;
hence x = y ; :: thesis: verum

end;

end;

end;

assume A2: for x, y being Element of X holds x = y ; :: thesis: X is trivial
let x, y be object ; :: according to ZFMISC_1:def 10 :: thesis: ( not x in X or not y in X or x = y )
assume A3: ( x in X & y in X ) ; :: thesis: x = y
reconsider x = x, y = y as set by TARSKI:1;
( x is Element of X & y is Element of X ) by Def1, A3;
hence x = y by A2; :: thesis: verum