:: deftheorem Def18 defines trivial STRUCT_0:def 18 :
for V being non empty ZeroStr holds
( V is trivial iff for u being Element of V holds u = 0. V );