for PTN being Petri_net
for M0 being Boolean_marking of PTN
for t being transition of PTN
for s being place of PTN st s in {t} *' holds
(Firing (t,M0)) . s = TRUE