:: deftheorem Def1 defines Trivial-COM COMPOS_1:def 8 :
for b₁ being strict COM-Struct holds
( b₁ = Trivial-COM iff the InstructionsF of b₁ = {[0,{},{}]} );