for P being set
for N being Petri_net of P
for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 concur R2 c= P1 concur P2