let P be set ; for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
let N be Petri_net of P; for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
let R1, R2, R3 be process of N; (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
thus
(R1 concur R2) concur R3 c= R1 concur (R2 concur R3)
XBOOLE_0:def 10 R1 concur (R2 concur R3) c= (R1 concur R2) concur R3proof
let x be
object ;
TARSKI:def 3 ( not x in (R1 concur R2) concur R3 or x in R1 concur (R2 concur R3) )
assume
x in (R1 concur R2) concur R3
;
x in R1 concur (R2 concur R3)
then consider C1 being
firing-sequence of
N such that A1:
x = C1
and A2:
ex
q1,
q2 being
FinSubsequence st
(
C1 = q1 \/ q2 &
q1 misses q2 &
Seq q1 in R1 concur R2 &
Seq q2 in R3 )
;
consider q1,
q2 being
FinSubsequence such that A3:
C1 = q1 \/ q2
and A4:
q1 misses q2
and A5:
Seq q1 in R1 concur R2
and A6:
Seq q2 in R3
by A2;
consider C2 being
firing-sequence of
N such that A7:
Seq q1 = C2
and A8:
ex
q3,
q4 being
FinSubsequence st
(
C2 = q3 \/ q4 &
q3 misses q4 &
Seq q3 in R1 &
Seq q4 in R2 )
by A5;
consider q3,
q4 being
FinSubsequence such that A9:
C2 = q3 \/ q4
and A10:
q3 misses q4
and A11:
Seq q3 in R1
and A12:
Seq q4 in R2
by A8;
consider n1 being
Nat such that A13:
dom q1 c= Seg n1
by FINSEQ_1:def 12;
A14:
q3 c= Seq q1
by A7, A9, XBOOLE_1:7;
A15:
q4 c= Seq q1
by A7, A9, XBOOLE_1:7;
Sgm (dom q1) is
one-to-one
by A13, FINSEQ_3:92;
then A16:
(Sgm (dom q1)) .: (dom q3) misses (Sgm (dom q1)) .: (dom q4)
by A10, A14, A15, FUNCT_1:66, FUNCT_1:112;
A17:
rng ((Sgm (dom q1)) | (dom q3)) = (Sgm (dom q1)) .: (dom q3)
by RELAT_1:115;
A18:
rng ((Sgm (dom q1)) | (dom q4)) = (Sgm (dom q1)) .: (dom q4)
by RELAT_1:115;
then A19:
q1 | (rng ((Sgm (dom q1)) | (dom q3))) misses q1 | (rng ((Sgm (dom q1)) | (dom q4)))
by A16, A17, RELAT_1:187;
A20:
dom (Sgm (dom q1)) =
dom (q3 \/ q4)
by A7, A9, FINSEQ_1:100
.=
(dom q3) \/ (dom q4)
by XTUPLE_0:23
;
A21:
(q1 | (rng ((Sgm (dom q1)) | (dom q3)))) \/ (q1 | (rng ((Sgm (dom q1)) | (dom q4)))) =
q1 | ((rng ((Sgm (dom q1)) | (dom q3))) \/ (rng ((Sgm (dom q1)) | (dom q4))))
by RELAT_1:78
.=
q1 | ((Sgm (dom q1)) .: ((dom q3) \/ (dom q4)))
by A17, A18, RELAT_1:120
.=
q1 | (rng ((Sgm (dom q1)) | (dom (Sgm (dom q1)))))
by A20, RELAT_1:115
.=
q1 | (rng (Sgm (dom q1)))
.=
q1 | (dom q1)
by FINSEQ_1:50
.=
q1
;
A22:
q1 c= C1
by A3, XBOOLE_1:7;
A23:
q1 | (rng ((Sgm (dom q1)) | (dom q3))) c= q1
by A21, XBOOLE_1:7;
A24:
q1 | (rng ((Sgm (dom q1)) | (dom q4))) c= q1
by A21, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2)
by A3, RELAT_1:12;
then A25:
rng q1 c= rng C1
by XBOOLE_1:7;
A26:
rng q1 = rng (Seq q1)
by FINSEQ_1:101;
A27:
rng (Seq q1) c= rng C1
by A25, FINSEQ_1:101;
A28:
rng (Seq q1) = (rng q3) \/ (rng q4)
by A7, A9, RELAT_1:12;
then A29:
rng q3 c= rng (Seq q1)
by XBOOLE_1:7;
rng q3 = rng (Seq q3)
by FINSEQ_1:101;
then A30:
rng (Seq q3) c= rng C1
by A27, A29;
A31:
rng q4 c= rng (Seq q1)
by A28, XBOOLE_1:7;
rng q4 = rng (Seq q4)
by FINSEQ_1:101;
then A32:
rng (Seq q4) c= rng C1
by A27, A31;
reconsider q5 =
q1 | (rng ((Sgm (dom q1)) | (dom q3))),
q6 =
q1 | (rng ((Sgm (dom q1)) | (dom q4))) as
FinSubsequence ;
reconsider fs =
C1 as
FinSequence of
rng C1 by FINSEQ_1:def 4;
reconsider fs1 =
Seq q1 as
FinSequence of
rng C1 by A25, A26, FINSEQ_1:def 4;
reconsider fs2 =
Seq q3 as
FinSequence of
rng C1 by A30, FINSEQ_1:def 4;
reconsider fs3 =
Seq q4 as
FinSequence of
rng C1 by A32, FINSEQ_1:def 4;
reconsider fss =
q1,
fss1 =
q5,
fss2 =
q6 as
Subset of
fs by A22, A23, A24, XBOOLE_1:1;
reconsider fss3 =
q3,
fss4 =
q4 as
Subset of
fs1 by A7, A9, XBOOLE_1:7;
A33:
Seq fss3 = fs2
;
fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3)))
;
then A34:
Seq q3 = Seq q5
by A33, FINSEQ_6:154;
A35:
Seq fss4 = fs3
;
A36:
fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4)))
;
q1 /\ q2 = {}
by A4;
then A37:
(q5 /\ q2) \/ (q6 /\ q2) = {}
by A21, XBOOLE_1:23;
then A38:
q5 /\ q2 = {}
;
q6 /\ q2 = {}
by A37;
then A39:
q6 misses q2
;
A40:
q1 c= C1
by A3, XBOOLE_1:7;
A41:
q2 c= C1
by A3, XBOOLE_1:7;
q6 c= q1
by A21, XBOOLE_1:7;
then
q6 c= C1
by A40;
then A42:
dom q6 misses dom q2
by A39, A41, FUNCT_1:112;
then reconsider q7 =
q6 \/ q2 as
Function by GRFUNC_1:13;
A43:
dom C1 =
(dom q1) \/ (dom q2)
by A3, XTUPLE_0:23
.=
((dom q5) \/ (dom q6)) \/ (dom q2)
by A21, XTUPLE_0:23
.=
(dom q5) \/ ((dom q6) \/ (dom q2))
by XBOOLE_1:4
.=
(dom q5) \/ (dom q7)
by XTUPLE_0:23
;
then A44:
dom q7 c= dom C1
by XBOOLE_1:7;
A45:
dom C1 = Seg (len C1)
by FINSEQ_1:def 3;
then reconsider q7 =
q7 as
FinSubsequence by A44, FINSEQ_1:def 12;
A46:
C1 = q5 \/ q7
by A3, A21, XBOOLE_1:4;
A47:
q5 /\ q7 = (q5 /\ q6) \/ (q5 /\ q2)
by XBOOLE_1:23;
q5 /\ q6 = {}
by A19;
then A48:
q5 misses q7
by A38, A47;
A49:
rng (Seq q7) = rng q7
by FINSEQ_1:101;
rng C1 = (rng q7) \/ (rng q5)
by A46, RELAT_1:12;
then A50:
rng (Seq q7) c= rng C1
by A49, XBOOLE_1:7;
rng C1 c= N
by FINSEQ_1:def 4;
then
rng (Seq q7) c= N
by A50;
then
Seq q7 is
FinSequence of
N
by FINSEQ_1:def 4;
then reconsider C3 =
Seq q7 as
firing-sequence of
N by FINSEQ_1:def 11;
A51:
dom (Seq q7) = Seg (len (Seq q7))
by FINSEQ_1:def 3;
A52:
dom (q6 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:25;
A53:
dom (q2 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:25;
A54:
dom (q6 * (Sgm (dom q7))) c= dom (Seq q7)
by A52, FINSEQ_1:100;
dom (q2 * (Sgm (dom q7))) c= dom (Seq q7)
by A53, FINSEQ_1:100;
then reconsider q8 =
q6 * (Sgm (dom q7)),
q9 =
q2 * (Sgm (dom q7)) as
FinSubsequence by A51, A54, FINSEQ_1:def 12;
A55:
C3 =
q7 * (Sgm (dom q7))
by FINSEQ_1:def 14
.=
q8 \/ q9
by RELAT_1:32
;
A56:
dom q8 = (Sgm (dom q7)) " (dom q6)
by RELAT_1:147;
A57:
dom q9 = (Sgm (dom q7)) " (dom q2)
by RELAT_1:147;
(dom q2) /\ (dom q6) = {}
by A42;
then
(Sgm (dom q7)) " ((dom q6) /\ (dom q2)) = {}
;
then
((Sgm (dom q7)) " (dom q6)) /\ ((Sgm (dom q7)) " (dom q2)) = {}
by FUNCT_1:68;
then A58:
(Sgm (dom q7)) " (dom q6) misses (Sgm (dom q7)) " (dom q2)
;
A59:
dom q6 c= (dom q6) \/ (dom q2)
by XBOOLE_1:7;
A60:
dom q2 c= (dom q6) \/ (dom q2)
by XBOOLE_1:7;
A61:
dom q6 c= dom q7
by A59, XTUPLE_0:23;
A62:
dom q2 c= dom q7
by A60, XTUPLE_0:23;
A63:
dom q6 c= rng (Sgm (dom q7))
by A61, FINSEQ_1:50;
A64:
dom q2 c= rng (Sgm (dom q7))
by A62, FINSEQ_1:50;
A65:
dom q8 = (Sgm (dom q7)) " (dom q6)
by RELAT_1:147;
A66:
dom q9 = (Sgm (dom q7)) " (dom q2)
by RELAT_1:147;
A67:
rng ((Sgm (dom q7)) | (dom q8)) =
rng ((dom q6) |` (Sgm (dom q7)))
by A65, FUNCT_1:113
.=
dom q6
by A63, RELAT_1:89
;
A68:
dom q8 c= dom (Sgm (dom q7))
by RELAT_1:25;
A69:
dom q9 c= dom (Sgm (dom q7))
by RELAT_1:25;
A70:
(Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8)))
by A43, A45, A68, FINSEQ_6:129, XBOOLE_1:7;
A71:
Seq q8 =
(q6 * (Sgm (dom q7))) * (Sgm (dom q8))
by FINSEQ_1:def 14
.=
q6 * ((Sgm (dom q7)) * (Sgm (dom q8)))
by RELAT_1:36
.=
Seq q6
by A67, A70, FINSEQ_1:def 14
;
A72:
rng ((Sgm (dom q7)) | (dom q9)) =
rng ((dom q2) |` (Sgm (dom q7)))
by A66, FUNCT_1:113
.=
dom q2
by A64, RELAT_1:89
;
A73:
(Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9)))
by A43, A45, A69, FINSEQ_6:129, XBOOLE_1:7;
A74:
Seq q9 =
(q2 * (Sgm (dom q7))) * (Sgm (dom q9))
by FINSEQ_1:def 14
.=
q2 * ((Sgm (dom q7)) * (Sgm (dom q9)))
by RELAT_1:36
.=
Seq q2
by A72, A73, FINSEQ_1:def 14
;
Seq q8 in R2
by A12, A35, A36, A71, FINSEQ_6:154;
then
ex
ss1,
ss2 being
FinSubsequence st
(
C3 = ss1 \/ ss2 &
ss1 misses ss2 &
Seq ss1 in R2 &
Seq ss2 in R3 )
by A6, A55, A56, A57, A58, A74, RELAT_1:179;
then
Seq q7 in R2 concur R3
;
hence
x in R1 concur (R2 concur R3)
by A1, A11, A34, A46, A48;
verum
end;
let x be object ; TARSKI:def 3 ( not x in R1 concur (R2 concur R3) or x in (R1 concur R2) concur R3 )
assume
x in R1 concur (R2 concur R3)
; x in (R1 concur R2) concur R3
then consider C1 being firing-sequence of N such that
A75:
x = C1
and
A76:
ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 concur R3 )
;
consider q1, q2 being FinSubsequence such that
A77:
C1 = q1 \/ q2
and
A78:
q1 misses q2
and
A79:
Seq q1 in R1
and
A80:
Seq q2 in R2 concur R3
by A76;
consider C2 being firing-sequence of N such that
A81:
Seq q2 = C2
and
A82:
ex q3, q4 being FinSubsequence st
( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 )
by A80;
consider q3, q4 being FinSubsequence such that
A83:
C2 = q3 \/ q4
and
A84:
q3 misses q4
and
A85:
Seq q3 in R2
and
A86:
Seq q4 in R3
by A82;
consider n1 being Nat such that
A87:
dom q2 c= Seg n1
by FINSEQ_1:def 12;
A88:
q3 c= Seq q2
by A81, A83, XBOOLE_1:7;
A89:
q4 c= Seq q2
by A81, A83, XBOOLE_1:7;
Sgm (dom q2) is one-to-one
by A87, FINSEQ_3:92;
then A90:
(Sgm (dom q2)) .: (dom q3) misses (Sgm (dom q2)) .: (dom q4)
by A84, A88, A89, FUNCT_1:66, FUNCT_1:112;
A91:
rng ((Sgm (dom q2)) | (dom q3)) = (Sgm (dom q2)) .: (dom q3)
by RELAT_1:115;
A92:
rng ((Sgm (dom q2)) | (dom q4)) = (Sgm (dom q2)) .: (dom q4)
by RELAT_1:115;
then A93:
q2 | (rng ((Sgm (dom q2)) | (dom q3))) misses q2 | (rng ((Sgm (dom q2)) | (dom q4)))
by A90, A91, RELAT_1:187;
A94: dom (Sgm (dom q2)) =
dom (Seq q2)
by FINSEQ_1:100
.=
(dom q3) \/ (dom q4)
by A81, A83, XTUPLE_0:23
;
A95: (q2 | (rng ((Sgm (dom q2)) | (dom q3)))) \/ (q2 | (rng ((Sgm (dom q2)) | (dom q4)))) =
q2 | ((rng ((Sgm (dom q2)) | (dom q3))) \/ (rng ((Sgm (dom q2)) | (dom q4))))
by RELAT_1:78
.=
q2 | ((Sgm (dom q2)) .: ((dom q3) \/ (dom q4)))
by A91, A92, RELAT_1:120
.=
q2 | (rng ((Sgm (dom q2)) | (dom (Sgm (dom q2)))))
by A94, RELAT_1:115
.=
q2 | (rng (Sgm (dom q2)))
.=
q2 | (dom q2)
by FINSEQ_1:50
.=
q2
;
A96:
q2 c= C1
by A77, XBOOLE_1:7;
A97:
q2 | (rng ((Sgm (dom q2)) | (dom q3))) c= q2
by A95, XBOOLE_1:7;
A98:
q2 | (rng ((Sgm (dom q2)) | (dom q4))) c= q2
by A95, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2)
by A77, RELAT_1:12;
then A99:
rng q2 c= rng C1
by XBOOLE_1:7;
A100:
rng q2 = rng (Seq q2)
by FINSEQ_1:101;
A101:
rng (Seq q2) c= rng C1
by A99, FINSEQ_1:101;
A102:
rng (Seq q2) = (rng q3) \/ (rng q4)
by A81, A83, RELAT_1:12;
then A103:
rng q3 c= rng (Seq q2)
by XBOOLE_1:7;
rng q3 = rng (Seq q3)
by FINSEQ_1:101;
then A104:
rng (Seq q3) c= rng C1
by A101, A103;
A105:
rng q4 c= rng (Seq q2)
by A102, XBOOLE_1:7;
rng q4 = rng (Seq q4)
by FINSEQ_1:101;
then A106:
rng (Seq q4) c= rng C1
by A101, A105;
reconsider q5 = q2 | (rng ((Sgm (dom q2)) | (dom q3))), q6 = q2 | (rng ((Sgm (dom q2)) | (dom q4))) as FinSubsequence ;
reconsider fs = C1 as FinSequence of rng C1 by FINSEQ_1:def 4;
reconsider fs1 = Seq q2 as FinSequence of rng C1 by A99, A100, FINSEQ_1:def 4;
reconsider fs2 = Seq q3 as FinSequence of rng C1 by A104, FINSEQ_1:def 4;
reconsider fs3 = Seq q4 as FinSequence of rng C1 by A106, FINSEQ_1:def 4;
reconsider fss = q2, fss1 = q5, fss2 = q6 as Subset of fs by A96, A97, A98, XBOOLE_1:1;
reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A81, A83, XBOOLE_1:7;
A107:
Seq fss3 = fs2
;
A108:
fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3)))
;
A109:
Seq fss4 = fs3
;
fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4)))
;
then A110:
Seq q4 = Seq q6
by A109, FINSEQ_6:154;
q1 /\ q2 = {}
by A78;
then A111:
(q1 /\ q5) \/ (q1 /\ q6) = {}
by A95, XBOOLE_1:23;
then A112:
q1 /\ q5 = {}
;
A113:
q1 /\ q6 = {}
by A111;
A114:
q1 misses q5
by A112;
A115:
q1 c= C1
by A77, XBOOLE_1:7;
A116:
q2 c= C1
by A77, XBOOLE_1:7;
q5 c= q2
by A95, XBOOLE_1:7;
then
q5 c= C1
by A116;
then A117:
dom q1 misses dom q5
by A114, A115, FUNCT_1:112;
then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:13;
A118: dom C1 =
(dom q1) \/ (dom q2)
by A77, XTUPLE_0:23
.=
(dom q1) \/ ((dom q5) \/ (dom q6))
by A95, XTUPLE_0:23
.=
((dom q1) \/ (dom q5)) \/ (dom q6)
by XBOOLE_1:4
.=
(dom q7) \/ (dom q6)
by XTUPLE_0:23
;
then A119:
dom q7 c= dom C1
by XBOOLE_1:7;
A120:
dom C1 = Seg (len C1)
by FINSEQ_1:def 3;
then reconsider q7 = q7 as FinSubsequence by A119, FINSEQ_1:def 12;
A121:
C1 = q7 \/ q6
by A77, A95, XBOOLE_1:4;
A122:
q7 /\ q6 = (q1 /\ q6) \/ (q5 /\ q6)
by XBOOLE_1:23;
q5 /\ q6 = {}
by A93;
then A123:
q7 misses q6
by A113, A122;
A124:
rng (Seq q7) = rng q7
by FINSEQ_1:101;
rng C1 = (rng q7) \/ (rng q6)
by A121, RELAT_1:12;
then A125:
rng (Seq q7) c= rng C1
by A124, XBOOLE_1:7;
rng C1 c= N
by FINSEQ_1:def 4;
then
rng (Seq q7) c= N
by A125;
then
Seq q7 is FinSequence of N
by FINSEQ_1:def 4;
then reconsider C3 = Seq q7 as firing-sequence of N by FINSEQ_1:def 11;
A126:
dom (Seq q7) = Seg (len (Seq q7))
by FINSEQ_1:def 3;
A127:
dom (q1 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:25;
A128:
dom (q5 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:25;
A129:
dom (q1 * (Sgm (dom q7))) c= dom (Seq q7)
by A127, FINSEQ_1:100;
dom (q5 * (Sgm (dom q7))) c= dom (Seq q7)
by A128, FINSEQ_1:100;
then reconsider q8 = q1 * (Sgm (dom q7)), q9 = q5 * (Sgm (dom q7)) as FinSubsequence by A126, A129, FINSEQ_1:def 12;
A130: C3 =
q7 * (Sgm (dom q7))
by FINSEQ_1:def 14
.=
q8 \/ q9
by RELAT_1:32
;
A131:
dom q8 = (Sgm (dom q7)) " (dom q1)
by RELAT_1:147;
A132:
dom q9 = (Sgm (dom q7)) " (dom q5)
by RELAT_1:147;
(dom q1) /\ (dom q5) = {}
by A117;
then
(Sgm (dom q7)) " ((dom q1) /\ (dom q5)) = {}
;
then
((Sgm (dom q7)) " (dom q1)) /\ ((Sgm (dom q7)) " (dom q5)) = {}
by FUNCT_1:68;
then A133:
(Sgm (dom q7)) " (dom q1) misses (Sgm (dom q7)) " (dom q5)
;
A134:
dom q1 c= (dom q1) \/ (dom q5)
by XBOOLE_1:7;
A135:
dom q5 c= (dom q1) \/ (dom q5)
by XBOOLE_1:7;
A136:
dom q1 c= dom q7
by A134, XTUPLE_0:23;
A137:
dom q5 c= dom q7
by A135, XTUPLE_0:23;
A138:
dom q1 c= rng (Sgm (dom q7))
by A136, FINSEQ_1:50;
A139:
dom q5 c= rng (Sgm (dom q7))
by A137, FINSEQ_1:50;
A140:
dom q8 = (Sgm (dom q7)) " (dom q1)
by RELAT_1:147;
A141:
dom q9 = (Sgm (dom q7)) " (dom q5)
by RELAT_1:147;
A142: rng ((Sgm (dom q7)) | (dom q8)) =
rng ((dom q1) |` (Sgm (dom q7)))
by A140, FUNCT_1:113
.=
dom q1
by A138, RELAT_1:89
;
A143:
dom q8 c= dom (Sgm (dom q7))
by RELAT_1:25;
A144:
dom q9 c= dom (Sgm (dom q7))
by RELAT_1:25;
A145:
(Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8)))
by A118, A120, A143, FINSEQ_6:129, XBOOLE_1:7;
A146: Seq q8 =
(q1 * (Sgm (dom q7))) * (Sgm (dom q8))
by FINSEQ_1:def 14
.=
q1 * ((Sgm (dom q7)) * (Sgm (dom q8)))
by RELAT_1:36
.=
Seq q1
by A142, A145, FINSEQ_1:def 14
;
A147: rng ((Sgm (dom q7)) | (dom q9)) =
rng ((dom q5) |` (Sgm (dom q7)))
by A141, FUNCT_1:113
.=
dom q5
by A139, RELAT_1:89
;
A148:
(Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9)))
by A118, A120, A144, FINSEQ_6:129, XBOOLE_1:7;
Seq q9 =
(q5 * (Sgm (dom q7))) * (Sgm (dom q9))
by FINSEQ_1:def 14
.=
q5 * ((Sgm (dom q7)) * (Sgm (dom q9)))
by RELAT_1:36
.=
Seq q5
by A147, A148, FINSEQ_1:def 14
;
then
Seq q9 in R2
by A85, A107, A108, FINSEQ_6:154;
then
ex ss1, ss2 being FinSubsequence st
( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R1 & Seq ss2 in R2 )
by A79, A130, A131, A132, A133, A146, RELAT_1:179;
then
Seq q7 in R1 concur R2
;
hence
x in (R1 concur R2) concur R3
by A75, A86, A110, A121, A123; verum