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