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

proof

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

end;

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