:: deftheorem defnontrivial defines with-nontrivial-ColoredSet PETRI_3:def 9 :
for CPN being Colored_PT_net_Str holds
( CPN is with-nontrivial-ColoredSet iff not the ColoredSet of CPN is trivial );