for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 *' = { (f `2) where f is T-S_arc of PTN : f `1 in T0 }