theorem :: PETRI:12

for PTN being Petri_net holds ({} the carrier' of PTN) *' = {}