:: deftheorem defines .: PETRI:def 14 :
for PTN being Petri_net
for s being place of PTN holds s .: = s;