for PTN being Petri_net
for t being transition of PTN
for S0 being Subset of the carrier of PTN holds
( t in *' S0 iff {t} *' meets S0 )