let PTN be PT_net_Str ; :: thesis: for T0 being Subset of the Transitions of PTN
for x being set holds
( x in T0 *' iff ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) )
let T0 be Subset of the Transitions of PTN; :: thesis: for x being set holds
( x in T0 *' iff ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) )
let x be set ; :: thesis: ( x in T0 *' iff ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) )
thus ( x in T0 *' implies ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) ) :: thesis: ( ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) implies x in T0 *' )

proof

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

end;

given f being T-S_arc of PTN, t being transition of PTN such that A5: ( t in T0 & f = [t,x] ) ; :: thesis: x in T0 *'
x = f `2 by A5, MCART_1:7;
hence x in T0 *' by A5; :: thesis: verum