theorem :: PNPROC_1:37

for P being set
for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)