:: deftheorem defines NeutralProcess PNPROC_1:def 14 :
for P being set
for N being Petri_net of P holds NeutralProcess N = {(<*> N)};