theorem Th34: :: PNPROC_1:34

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