:: deftheorem Def9 defines trivial STRUCT_0:def 9 :
for IT being 1-sorted holds
( IT is trivial iff the carrier of IT is trivial );