theorem :: PETRI:9

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