theorem :: PETRI_2:6

for CPNT being Colored_Petri_net
for t being transition of CPNT st CPNT is Colored-PT-net-like & t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ;