set R = P pcs-times Q;
set TR = the ToleranceRel of (P pcs-times Q);
set D1 = the carrier of P;
set D2 = the carrier of Q;
let p, p9, q, q9 be Element of (P pcs-times Q); PCS_0:def 22 ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume that
A1:
p (--) q
and
A2:
p9 <= p
and
A3:
q9 <= q
; p9 (--) q9
A4:
[p,q] in the ToleranceRel of (P pcs-times Q)
by A1;
then consider a, b, c, d being set such that
A5:
p = [a,b]
and
A6:
q = [c,d]
and
A7:
a in the carrier of P
and
A8:
b in the carrier of Q
and
A9:
c in the carrier of P
and
A10:
d in the carrier of Q
and
( [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q )
by Def2;
A11:
[p9,p] in the InternalRel of (P pcs-times Q)
by A2;
then
p9 in the carrier of (P pcs-times Q)
by ZFMISC_1:87;
then consider e, f being object such that
A12:
e in the carrier of P
and
A13:
f in the carrier of Q
and
A14:
p9 = [e,f]
by ZFMISC_1:def 2;
A15:
[q9,q] in the InternalRel of (P pcs-times Q)
by A3;
then
q9 in the carrier of (P pcs-times Q)
by ZFMISC_1:87;
then consider g, h being object such that
A16:
g in the carrier of P
and
A17:
h in the carrier of Q
and
A18:
q9 = [g,h]
by ZFMISC_1:def 2;
reconsider P = P, Q = Q as non empty pcs-compatible pcs-Str by A7, A8;
reconsider a = a, c = c, e = e, g = g as Element of P by A7, A9, A12, A16;
reconsider b = b, d = d, f = f, h = h as Element of Q by A8, A10, A13, A17;
[^a,b^] (--) [^c,d^]
by A4, A5, A6;
then A19:
( a (--) c or b (--) d )
by Th6;
A20:
RelStr(# the carrier of (P pcs-times Q), the InternalRel of (P pcs-times Q) #) = [:P,Q:]
by YELLOW_3:def 2;
then A21:
[e,f] <= [a,b]
by A5, A11, A14;
then A22:
e <= a
by YELLOW_3:11;
A23:
f <= b
by A21, YELLOW_3:11;
A24:
[g,h] <= [c,d]
by A6, A15, A18, A20;
then A25:
g <= c
by YELLOW_3:11;
h <= d
by A24, YELLOW_3:11;
then
( e (--) g or f (--) h )
by A19, A22, A23, A25, Def22;
then A26:
( [e,g] in the ToleranceRel of P or [f,h] in the ToleranceRel of Q )
;
A27:
p9 = [e,f]
by A14;
q9 = [g,h]
by A18;
hence
[p9,q9] in the ToleranceRel of (P pcs-times Q)
by A26, A27, Def3; PCS_0:def 7 verum