theorem Th2: :: PETRI:2

for PTN being Petri_net
for S0 being Subset of the carrier of PTN
for x being object holds
( x in *' S0 iff ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [x,s] ) )