theorem :: PNPROC_1:42

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