:: deftheorem defines ElementaryProcess PNPROC_1:def 15 :
for P being set
for N being Petri_net of P
for t being Element of N holds ElementaryProcess t = {<*t*>};