theorem Th15: :: PETRI:15

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