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 Z: 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
let x, y be Element of the carrier of S; :: thesis: x = y
thus x = y by Z, A1, ZFMISC_1:def 10; :: thesis: verum

end;

assume A4: for x, y being Element of the carrier of S holds x = y ; :: thesis: S is trivial
let x, y be set ; :: according to ZFMISC_1:def 10,STRUCT_0:def 9 :: thesis: ( not x in the carrier of S or not y in the carrier of S or x = y )
thus ( not x in the carrier of S or not y in the carrier of S or x = y ) by A4; :: 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 1
.= y by A5, SUBSET_1:def 1 ; :: thesis: verum

end;

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

end;

end;