:: deftheorem defines *' PETRI:def 4 :
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 T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [t,s] ) } ;