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, p', q, q' be Element of ; PCS_0:def 22 ( p (--) q & p' <= p & q' <= q implies p' (--) q' )
assume that
A2:
p (--) q
and
A3:
p' <= p
and
A4:
q' <= q
; p' (--) q'
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, Def7;
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
;
p' (--) q'then A8:
p in the
carrier of
P
by ZFMISC_1:106;
A9:
q in the
carrier of
P
by A7, ZFMISC_1:106;
reconsider p1 =
p,
q1 =
q as
Element of
by A7, ZFMISC_1:106;
A10:
p1 (--) q1
by A7, Def7;
A11:
[p',p] in the
InternalRel of
P \/ the
InternalRel of
Q
by A3, A5, ORDERS_2:def 9;
A12:
[q',q] in the
InternalRel of
P \/ the
InternalRel of
Q
by A4, A5, ORDERS_2:def 9;
then reconsider p'1 =
p',
q'1 =
q' as
Element of
by A1, A8, A9, A11, Lm1;
A13:
[p',p] in the
InternalRel of
P
by A1, A8, A11, Lm1;
A14:
[q',q] in the
InternalRel of
P
by A1, A9, A12, Lm1;
A15:
p'1 <= p1
by A13, ORDERS_2:def 9;
q'1 <= q1
by A14, ORDERS_2:def 9;
then
p'1 (--) q'1
by A10, A15, Def22;
then
[p'1,q'1] in the
ToleranceRel of
P
by Def7;
then
[p'1,q'1] in the
ToleranceRel of
P \/ the
ToleranceRel of
Q
by XBOOLE_0:def 3;
hence
p' (--) q'
by A5, Def7;
verum end; suppose A16:
[p,q] in the
ToleranceRel of
Q
;
p' (--) q'then A17:
p in the
carrier of
Q
by ZFMISC_1:106;
A18:
q in the
carrier of
Q
by A16, ZFMISC_1:106;
reconsider p1 =
p,
q1 =
q as
Element of
by A16, ZFMISC_1:106;
A19:
p1 (--) q1
by A16, Def7;
A20:
[p',p] in the
InternalRel of
P \/ the
InternalRel of
Q
by A3, A5, ORDERS_2:def 9;
A21:
[q',q] in the
InternalRel of
P \/ the
InternalRel of
Q
by A4, A5, ORDERS_2:def 9;
then reconsider p'1 =
p',
q'1 =
q' as
Element of
by A1, A17, A18, A20, Lm1;
A22:
[p',p] in the
InternalRel of
Q
by A1, A17, A20, Lm1;
A23:
[q',q] in the
InternalRel of
Q
by A1, A18, A21, Lm1;
A24:
p'1 <= p1
by A22, ORDERS_2:def 9;
q'1 <= q1
by A23, ORDERS_2:def 9;
then
p'1 (--) q'1
by A19, A24, Def22;
then
[p'1,q'1] in the
ToleranceRel of
Q
by Def7;
then
[p'1,q'1] in the
ToleranceRel of
P \/ the
ToleranceRel of
Q
by XBOOLE_0:def 3;
hence
p' (--) q'
by A5, Def7;
verum end;