let P, Q be pcs; :: thesis: ( 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
; :: according to TSEP_1:def 3 :: thesis: pcs-sum P,Q is pcs-compatible
let p, p', q, q' be Element of (pcs-sum P,Q); :: according to PCS_0:def 22 :: thesis: ( p (--) q & p' <= p & q' <= q implies p' (--) q' )
assume that
A2:
p (--) q
and
A3:
p' <= p
and
A4:
q' <= q
; :: thesis: 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
;
:: thesis: p' (--) q'then A8:
(
p in the
carrier of
P &
q in the
carrier of
P )
by ZFMISC_1:106;
reconsider p1 =
p,
q1 =
q as
Element of
P by A7, ZFMISC_1:106;
A9:
p1 (--) q1
by A7, Def7;
A10:
(
[p',p] in the
InternalRel of
P \/ the
InternalRel of
Q &
[q',q] in the
InternalRel of
P \/ the
InternalRel of
Q )
by A3, A4, A5, ORDERS_2:def 9;
then reconsider p'1 =
p',
q'1 =
q' as
Element of
P by A1, A8, Lm1;
(
[p',p] in the
InternalRel of
P &
[q',q] in the
InternalRel of
P )
by A1, A8, A10, Lm1;
then
(
p'1 <= p1 &
q'1 <= q1 )
by ORDERS_2:def 9;
then
p'1 (--) q'1
by A9, 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;
:: thesis: verum end; suppose A11:
[p,q] in the
ToleranceRel of
Q
;
:: thesis: p' (--) q'then A12:
(
p in the
carrier of
Q &
q in the
carrier of
Q )
by ZFMISC_1:106;
reconsider p1 =
p,
q1 =
q as
Element of
Q by A11, ZFMISC_1:106;
A13:
p1 (--) q1
by A11, Def7;
A14:
(
[p',p] in the
InternalRel of
P \/ the
InternalRel of
Q &
[q',q] in the
InternalRel of
P \/ the
InternalRel of
Q )
by A3, A4, A5, ORDERS_2:def 9;
then reconsider p'1 =
p',
q'1 =
q' as
Element of
Q by A1, A12, Lm1;
(
[p',p] in the
InternalRel of
Q &
[q',q] in the
InternalRel of
Q )
by A1, A12, A14, Lm1;
then
(
p'1 <= p1 &
q'1 <= q1 )
by ORDERS_2:def 9;
then
p'1 (--) q'1
by A13, 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;
:: thesis: verum end;