theorem Th31: :: PNPROC_1:31

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