set I = the carrier of S;
per cases ( not the carrier of S is empty or the carrier of S is empty ) ;
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 )
proof
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;
assume A3: for x, y being Element of the carrier of S holds x = y ; :: thesis: 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;
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
proof
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;
hence ( S is trivial iff for x, y being Element of S holds x = y ) by A4; :: thesis: verum
end;
end;