let CPN be with-nontrivial-ColoredSet Colored-PT-net; :: thesis: 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) )
let m be colored-state of CPN; :: thesis: 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) )
let t be Element of the carrier' of CPN; :: thesis: 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) )
let D be thin_cylinder of the ColoredSet of CPN, *' {t}; :: thesis: ( ex ColD being color-threshold of D st t is_firable_on m,ColD iff D in firable_set_on (m,t) )
thus ( ex ColD being color-threshold of D st t is_firable_on m,ColD implies D in firable_set_on (m,t) ) ; :: thesis: ( D in firable_set_on (m,t) implies ex ColD being color-threshold of D st t is_firable_on m,ColD )
assume D in firable_set_on (m,t) ; :: thesis: ex ColD being color-threshold of D st t is_firable_on m,ColD
then ex D0 being thin_cylinder of the ColoredSet of CPN, *' {t} st
( D = D0 & ex ColD being color-threshold of D0 st t is_firable_on m,ColD ) ;
hence ex ColD being color-threshold of D st t is_firable_on m,ColD ; :: thesis: verum