theorem :: PETRI_3:6

for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for N being Function of I,(bool (rng CPNT))
for O being connecting-mapping of CPNT st CPNT is one-to-one & N,O is_Cell-Petri-nets holds
for i being Element of I holds not CPNT . i in N . i