theorem :: PETRI:10

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