theorem Th4: :: PETRI:4

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 S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] ) )