:: deftheorem defines .: PETRI:def 17 :
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 .: = T0;