let P be set ; :: thesis: for N being Petri_net of P
for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

let N be Petri_net of P; :: thesis: for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)
let R1, R2, P1, P2 be process of N; :: thesis: (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 concur R2) before (P1 concur P2) or x in (R1 before P1) concur (R2 before P2) )
assume x in (R1 concur R2) before (P1 concur P2) ; :: thesis: x in (R1 before P1) concur (R2 before P2)
then consider C1, C2 being firing-sequence of N such that
A1: x = C1 ^ C2 and
A2: C1 in R1 concur R2 and
A3: C2 in P1 concur P2 ;
consider C3 being firing-sequence of N such that
A4: C1 = C3 and
A5: ex q1, q2 being FinSubsequence st
( C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) by A2;
consider q1, q2 being FinSubsequence such that
A6: C3 = q1 \/ q2 and
A7: q1 misses q2 and
A8: Seq q1 in R1 and
A9: Seq q2 in R2 by A5;
consider C4 being firing-sequence of N such that
A10: C2 = C4 and
A11: ex q3, q4 being FinSubsequence st
( C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 & Seq q4 in P2 ) by A3;
consider q3, q4 being FinSubsequence such that
A12: C4 = q3 \/ q4 and
A13: q3 misses q4 and
A14: Seq q3 in P1 and
A15: Seq q4 in P2 by A11;
reconsider C = C1 ^ C2 as firing-sequence of N ;
reconsider q5 = (len C1) Shift q3, q6 = (len C1) Shift q4 as FinSubsequence ;
A16: q1 c= C1 by ;
A17: q2 c= C1 by ;
A18: q3 c= C2 by ;
A19: q4 c= C2 by ;
A20: C1 c= C1 ^ C2 by FINSEQ_6:10;
then A21: q1 c= C1 ^ C2 by A16;
A22: q2 c= C1 ^ C2 by ;
reconsider ss = C2 as FinSubsequence ;
A23: q5 c= (len C1) Shift ss by ;
A24: q6 c= (len C1) Shift ss by ;
A25: (len C1) Shift C2 c= C1 ^ C2 by VALUED_1:53;
then A26: q5 c= C1 ^ C2 by A23;
A27: q6 c= C1 ^ C2 by ;
A28: dom q1 misses dom q5 by ;
dom q2 misses dom q6 by ;
then reconsider ss1 = q1 \/ q5, ss2 = q2 \/ q6 as Function by ;
A29: dom C = Seg (len C) by FINSEQ_1:def 3;
A30: dom ss1 c= dom C by ;
dom ss2 c= dom C by ;
then reconsider ss1 = ss1, ss2 = ss2 as FinSubsequence by ;
A31: ss1 \/ ss2 = ((q1 \/ ((len C1) Shift q3)) \/ q2) \/ ((len C1) Shift q4) by XBOOLE_1:4
.= ((q1 \/ q2) \/ ((len C1) Shift q3)) \/ ((len C1) Shift q4) by XBOOLE_1:4
.= C1 \/ (((len C1) Shift q3) \/ ((len C1) Shift q4)) by
.= C1 \/ ((len C1) Shift C2) by
.= C by VALUED_1:49 ;
A32: ss1 /\ q2 = (q1 /\ q2) \/ (((len C1) Shift q3) /\ q2) by XBOOLE_1:23;
ss1 /\ ((len C1) Shift q4) = (q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4)) by XBOOLE_1:23;
then A33: ss1 /\ ss2 = ((q1 /\ q2) \/ (((len C1) Shift q3) /\ q2)) \/ ((q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4))) by ;
A34: q1 /\ q2 = {} by A7;
A35: (len C1) Shift q3 misses q2 by ;
A36: q1 misses (len C1) Shift q4 by ;
A37: ((len C1) Shift q3) /\ q2 = {} by A35;
A38: q1 /\ ((len C1) Shift q4) = {} by A36;
dom q3 misses dom q4 by ;
then dom ((len C1) Shift q3) misses dom ((len C1) Shift q4) by VALUED_1:54;
then (len C1) Shift q3 misses (len C1) Shift q4 by RELAT_1:179;
then ss1 /\ ss2 = {} by A33, A34, A37, A38;
then A39: ss1 misses ss2 ;
A40: ex ss3 being FinSubsequence st
( ss3 = ss1 & (Seq q1) ^ (Seq q3) = Seq ss3 ) by ;
A41: ex ss4 being FinSubsequence st
( ss4 = ss2 & (Seq q2) ^ (Seq q4) = Seq ss4 ) by ;
A42: Seq ss1 in R1 before P1 by A8, A14, A40;
Seq ss2 in R2 before P2 by A9, A15, A41;
hence x in (R1 before P1) concur (R2 before P2) by A1, A31, A39, A42; :: thesis: verum