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