for PTN being Petri_net
for M0 being Boolean_marking of PTN
for t being transition of PTN holds
( t is_firable_on M0 iff <*t*> is_firable_on M0 )