let P, Q be pcs; ( P misses Q implies pcs-sum (P,Q) is pcs-compatible )
set D1 = the carrier of P;
set D2 = the carrier of Q;
set R1 = the InternalRel of P;
set R2 = the InternalRel of Q;
set T1 = the ToleranceRel of P;
set T2 = the ToleranceRel of Q;
set R = the InternalRel of P \/ the InternalRel of Q;
set T = the ToleranceRel of P \/ the ToleranceRel of Q;
assume A1:
the carrier of P misses the carrier of Q
; TSEP_1:def 3 pcs-sum (P,Q) is pcs-compatible
let p, p9, q, q9 be Element of (pcs-sum (P,Q)); PCS_0:def 22 ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume that
A2:
p (--) q
and
A3:
p9 <= p
and
A4:
q9 <= q
; p9 (--) q9
A5:
pcs-sum (P,Q) = H1(P,Q)
by Th15;
then A6:
[p,q] in the ToleranceRel of P \/ the ToleranceRel of Q
by A2;
per cases
( [p,q] in the ToleranceRel of P or [p,q] in the ToleranceRel of Q )
by A6, XBOOLE_0:def 3;
suppose A7:
[p,q] in the
ToleranceRel of
P
;
p9 (--) q9then A8:
p in the
carrier of
P
by ZFMISC_1:87;
A9:
q in the
carrier of
P
by A7, ZFMISC_1:87;
reconsider p1 =
p,
q1 =
q as
Element of
P by A7, ZFMISC_1:87;
A10:
p1 (--) q1
by A7;
A11:
[p9,p] in the
InternalRel of
P \/ the
InternalRel of
Q
by A3, A5;
A12:
[q9,q] in the
InternalRel of
P \/ the
InternalRel of
Q
by A4, A5;
then reconsider p91 =
p9,
q91 =
q9 as
Element of
P by A1, A8, A9, A11, Lm1;
A13:
[p9,p] in the
InternalRel of
P
by A1, A8, A11, Lm1;
A14:
[q9,q] in the
InternalRel of
P
by A1, A9, A12, Lm1;
A15:
p91 <= p1
by A13;
q91 <= q1
by A14;
then
p91 (--) q91
by A10, A15, Def22;
then
[p91,q91] in the
ToleranceRel of
P
;
then
[p91,q91] in the
ToleranceRel of
P \/ the
ToleranceRel of
Q
by XBOOLE_0:def 3;
hence
p9 (--) q9
by A5;
verum end; suppose A16:
[p,q] in the
ToleranceRel of
Q
;
p9 (--) q9then A17:
p in the
carrier of
Q
by ZFMISC_1:87;
A18:
q in the
carrier of
Q
by A16, ZFMISC_1:87;
reconsider p1 =
p,
q1 =
q as
Element of
Q by A16, ZFMISC_1:87;
A19:
p1 (--) q1
by A16;
A20:
[p9,p] in the
InternalRel of
P \/ the
InternalRel of
Q
by A3, A5;
A21:
[q9,q] in the
InternalRel of
P \/ the
InternalRel of
Q
by A4, A5;
then reconsider p91 =
p9,
q91 =
q9 as
Element of
Q by A1, A17, A18, A20, Lm1;
A22:
[p9,p] in the
InternalRel of
Q
by A1, A17, A20, Lm1;
A23:
[q9,q] in the
InternalRel of
Q
by A1, A18, A21, Lm1;
A24:
p91 <= p1
by A22;
q91 <= q1
by A23;
then
p91 (--) q91
by A19, A24, Def22;
then
[p91,q91] in the
ToleranceRel of
Q
;
then
[p91,q91] in the
ToleranceRel of
P \/ the
ToleranceRel of
Q
by XBOOLE_0:def 3;
hence
p9 (--) q9
by A5;
verum end;