theorem Th6: :: PETRI:6

for PTN being Petri_net
for T0 being Subset of the carrier' of PTN
for x being set holds
( x in *' T0 iff ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [x,t] ) )