let PTN be Petri_net; :: thesis: 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] ) )
let S0 be Subset of the carrier of PTN; :: thesis: 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] ) )
let x be object ; :: thesis: ( 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] ) )
thus ( x in S0 *' implies ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] ) ) :: thesis: ( ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] ) implies x in S0 *' )

proof

assume x in S0 *' ; :: thesis: ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] )
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] ) ;
consider f being S-T_arc of PTN, s being place of PTN such that
A3: ( s in S0 & f = [s,t] ) by A2;
take f ; :: thesis: ex s being place of PTN st
( s in S0 & f = [s,x] )
take s ; :: thesis: ( s in S0 & f = [s,x] )
thus ( s in S0 & f = [s,x] ) by A1, A3; :: thesis: verum

end;

given f being S-T_arc of PTN, s being place of PTN such that A4: s in S0 and
A5: f = [s,x] ; :: thesis: x in S0 *'
x = f `2 by A5;
hence x in S0 *' by A4, A5; :: thesis: verum