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