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