:: deftheorem defines nat_marks_of PETRI_DF:def 5 :
for N being PT_net_Str holds nat_marks_of N = Funcs ( the carrier of N,NAT);