for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN holds
( t is_firable_at M0 iff <*t*> is_firable_at M0 )