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 .: 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 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
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