:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMISTD_4:def 2 :
for N being with_zero set
for A being non empty with_non-empty_values AMI-Struct over N holds
( A is with_non_trivial_ObjectKinds iff for o being Object of A holds not Values o is trivial );