for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 c= R1 concur R2