:: deftheorem defines before PNPROC_1:def 12 :
for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 = { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;