set I = the carrier of S;

per cases ( not the carrier of S is empty or the carrier of S is empty ) ;

suppose A1: not the carrier of S is empty ; :: thesis: ( S is trivial iff for x, y being Element of S holds x = y )

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

proof

assume the carrier of S is trivial ; :: according to STRUCT_0:def 9 :: thesis: for x, y being Element of the carrier of S holds x = y
then consider a being set such that
A2: the carrier of S = {a} by A1, REALSET1:def 4;
let x, y be Element of the carrier of S; :: thesis: x = y
thus x = a by A2, TARSKI:def 1
.= y by A2, TARSKI:def 1 ; :: thesis: verum

end;

consider a being set such that
A3: a in the carrier of S by A1, XBOOLE_0:def 1;
assume A4: for x, y being Element of the carrier of S holds x = y ; :: thesis: S is trivial
the carrier of S = {a}

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: R14({a}, the carrier of S)

let i be set ; :: thesis: ( i in the carrier of S implies i in {a} )
assume i in the carrier of S ; :: thesis: i in {a}
then a = i by A4, A3;
hence i in {a} by TARSKI:def 1; :: thesis: verum

end;

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in {a} or i in the carrier of S )
assume i in {a} ; :: thesis: i in the carrier of S
hence i in the carrier of S by A3, TARSKI:def 1; :: thesis: verum

end;

hence ( the carrier of S is empty or ex x being set st the carrier of S = {x} ) ; :: according to REALSET1:def 4,STRUCT_0:def 9 :: thesis: verum

end;

suppose A5: the carrier of S is empty ; :: thesis: ( S is trivial iff for x, y being Element of S holds x = y )

for x, y being Element of the carrier of S holds x = y

proof

let x, y be Element of the carrier of S; :: thesis: x = y
thus x = {} by A5, SUBSET_1:def 2
.= y by A5, SUBSET_1:def 2 ; :: thesis: verum

end;

hence ( S is trivial iff for x, y being Element of S holds x = y ) by A5; :: thesis: verum

end;

end;