theorem Th16: :: PETRI:16

for PTN being Petri_net
for S being Subset of the carrier of PTN holds *' (S .:) = S *'