let P, Q be pcs-Str ; :: thesis: for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 holds
q1 (--) q2
let p, q be Element of (P --> Q); :: thesis: for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 holds
q1 (--) q2
let p1, p2 be Element of P; :: thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 holds
q1 (--) q2
let q1, q2 be Element of Q; :: thesis: ( p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 implies q1 (--) q2 )
assume that
A1: p = [p1,q1] and
A2: q = [p2,q2] ; :: thesis: ( not p (--) q or not p1 (--) p2 or q1 (--) q2 )
reconsider r1 = p1, r2 = p2 as Element of (pcs-reverse P) by Def40;
assume [p,q] in the ToleranceRel of (P --> Q) ; :: according to PCS_0:def 7 :: thesis: ( not p1 (--) p2 or q1 (--) q2 )
then consider a, b, s, t being set such that
A3: p = [a,b] and
A4: q = [s,t] and
a in the carrier of (pcs-reverse P) and
b in the carrier of Q and
s in the carrier of (pcs-reverse P) and
t in the carrier of Q and
A5: ( [a,s] in the ToleranceRel of (pcs-reverse P) or [b,t] in the ToleranceRel of Q ) by Def2;
A6: a = p1 by A1, A3, XTUPLE_0:1;
A7: b = q1 by A1, A3, XTUPLE_0:1;
A8: s = p2 by A2, A4, XTUPLE_0:1;
t = q2 by A2, A4, XTUPLE_0:1;
then ( r1 (--) r2 or q1 (--) q2 ) by A5, A6, A7, A8;
hence ( not p1 (--) p2 or q1 (--) q2 ) by Th34; :: thesis: verum