theorem :: PNPROC_1:40

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 before R2 c= P1 before P2