theorem Th29: :: PNPROC_1:29

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