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