for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D being thin_cylinder of the ColoredSet of CPN, *' {t} holds
( ex ColD being color-threshold of D st t is_firable_on m,ColD iff D in firable_set_on (m,t) )