:: deftheorem defines disjoint_valued PETRI_3:def 2 :
for I being non empty set
for CPNT being Colored-PT-net-Family of I holds
( CPNT is disjoint_valued iff for i, j being Element of I st i <> j holds
( the carrier of (CPNT . i) misses the carrier of (CPNT . j) & the carrier' of (CPNT . i) misses the carrier' of (CPNT . j) ) );