for PTN being Petri_net
for M0 being marking of PTN
for Q, Q1 being FinSequence of the carrier' of PTN st Q ^ Q1 is_firable_at M0 holds
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )