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 )