let PTN be Petri_net; :: thesis: for S being Subset of the carrier of PTN holds *' (S .:) = S *'
let S be Subset of the carrier of PTN; :: thesis: *' (S .:) = S *'
thus *' (S .:) c= S *' :: according to XBOOLE_0:def 10 :: thesis: S *' c= *' (S .:)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in *' (S .:) or x in S *' )
assume x in *' (S .:) ; :: thesis: x in S *'
then consider f being T-S_arc of (PTN .:), s being place of (PTN .:) such that
A1: s in S .: and
A2: f = [x,s] by Th2;
[(.: s),x] is S-T_arc of PTN by A2, RELAT_1:def 7;
hence x in S *' by A1, Th4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S *' or x in *' (S .:) )
assume x in S *' ; :: thesis: x in *' (S .:)
then consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S and
A4: f = [s,x] by Th4;
[x,(s .:)] is T-S_arc of (PTN .:) by A4, RELAT_1:def 7;
hence x in *' (S .:) by A3, Th2; :: thesis: verum