:: deftheorem Def10 defines trivial STRUCT_0:def 10 :
for S being 1-sorted holds
( S is trivial iff for x, y being Element of S holds x = y );