let P be set ; :: thesis: for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 c= R1 concur R2
let N be Petri_net of P; :: thesis: for R1, R2 being process of N holds R1 before R2 c= R1 concur R2
let R1, R2 be process of N; :: thesis: R1 before R2 c= R1 concur R2
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 before R2 or x in R1 concur R2 )
assume A1: x in R1 before R2 ; :: thesis: x in R1 concur R2
then reconsider C = x as firing-sequence of N ;
consider C1, C2 being firing-sequence of N such that
A2: ( x = C1 ^ C2 & C1 in R1 & C2 in R2 ) by A1;
set q1 = C1;
set q2 = (len C1) Shift C2;
reconsider q1 = C1 as FinSequence ;
( C = q1 \/ ((len C1) Shift C2) & q1 misses (len C1) Shift C2 & Seq q1 in R1 & Seq ((len C1) Shift C2) in R2 ) by A2, Th61, Th64, Th65, FINSEQ_3:125;
hence x in R1 concur R2 ; :: thesis: verum