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

proof

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

end;

given f being S-T_arc of PTN, t being transition of PTN such that A4: t in T0 and
A5: f = [x,t] ; :: thesis: x in *' T0
x = f `1 by A5;
hence x in *' T0 by A4, A5; :: thesis: verum