theorem :: PETRI:3

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