theorem :: PETRI:11

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