let PTN be PT_net_Str ; :: thesis: for T0 being Subset of the Transitions of PTN holds *' T0 = { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 }
let T0 be Subset of the Transitions of PTN; :: thesis: *' T0 = { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 }
thus *' T0 c= { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 } :: according to XBOOLE_0:def 10 :: thesis: { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 } c= *' T0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in *' T0 or x in { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 } )
assume x in *' T0 ; :: thesis: x in { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 }
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 and
A4: f = [s,t] by A2;
( f `1 = s & f `2 = t ) by A4, MCART_1:7;
hence x in { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 } by A1, A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 } or x in *' T0 )
assume x in { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 } ; :: thesis: x in *' T0
then consider f being S-T_arc of PTN such that
A5: x = f `1 and
A6: f `2 in T0 ;
f = [(f `1 ),(f `2 )] by MCART_1:23;
hence x in *' T0 by A5, A6; :: thesis: verum