:: deftheorem defines *' PETRI:def 5 :
for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds S0 *' = { t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] ) } ;