set I = the carrier of S;

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

end;

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

let x, y be object ; :: 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 A3; :: thesis: verum

end;proof

assume A3:
for x, y being Element of the carrier of S holds x = y
; :: thesis: S is trivial
assume A2:
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 A2; :: thesis: verum

end;let x, y be Element of the carrier of S; :: thesis: x = y

thus x = y by A2; :: thesis: verum

let x, y be object ; :: 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 A3; :: thesis: verum

suppose A4:
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

end;proof

hence
( S is trivial iff for x, y being Element of S holds x = y )
by A4; :: thesis: verum
let x, y be Element of the carrier of S; :: thesis: x = y

thus x = {} by A4, SUBSET_1:def 1

.= y by A4, SUBSET_1:def 1 ; :: thesis: verum

end;thus x = {} by A4, SUBSET_1:def 1

.= y by A4, SUBSET_1:def 1 ; :: thesis: verum