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 ) ;
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