theorem :: PNPROC_1:33

for P being set
for N being Petri_net of P
for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}