theorem :: PNPROC_1:32

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