:: deftheorem defines .: PETRI:def 18 :
for PTN being Petri_net
for t being transition of PTN holds t .: = t;