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