:: deftheorem Def21 defines trivial' STRUCT_0:def 21 :
for S being 2-sorted holds
( S is trivial' iff the carrier' of S is trivial );