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

assume X is trivial ; :: thesis: for x, y being Element of X holds x = y
then consider w being set such that
A1: X = {w} by REALSET1:def 4;
let x, y be Element of X; :: thesis: x = y
( x = w & y = w ) by A1, TARSKI:def 1;
hence x = y ; :: thesis: verum

end;

assume A2: for x, y being Element of X holds x = y ; :: thesis: X is trivial
consider w being set such that
A3: w in X by XBOOLE_0:def 1;
for z being set holds
( z in X iff z = w ) by A2, A3;
then X = {w} by TARSKI:def 1;
hence X is trivial by REALSET1:def 4; :: thesis: verum