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

proof

let x be set ; :: 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 .: & f = [x,s] ) by Th2;
[(.: s),x] is S-T_arc of PTN by A1, RELAT_1:def 7;
hence x in S *' by A1, Th4; :: thesis: verum

end;

let x be set ; :: 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
A2: ( s in S & f = [s,x] ) by Th4;
[x,(s .: )] is T-S_arc of (PTN .: ) by A2, RELAT_1:def 7;
hence x in *' (S .: ) by A2, Th2; :: thesis: verum