:: deftheorem defines Cell-Petri-nets PETRI_3:def 7 :
for I being non empty finite set
for CPNT being Colored-PT-net-Family of I holds
( CPNT is Cell-Petri-nets iff ex N being Function of I,(bool (rng CPNT)) st
for i being Element of I holds N . i = { (CPNT . j) where j is Element of I : j <> i } );