theorem :: PNPROC_1:44

for P being set
for N being Petri_net of P
for R being process of N holds R before (NeutralProcess N) = R