:: deftheorem Def9 defines Petri_net PNPROC_1:def 9 :
for P being set
for b₂ being non empty set holds
( b₂ is Petri_net of P iff for x being set st x in b₂ holds
x is transition of P );