theorem :: PETRI:5

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