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 A1: ( p = [p1,q1] & 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
A2: ( p = [a,b] & q = [s,t] ) and
( a in the carrier of (pcs-reverse P) & b in the carrier of Q & s in the carrier of (pcs-reverse P) & t in the carrier of Q ) and
A3: ( [a,s] in the ToleranceRel of (pcs-reverse P) or [b,t] in the ToleranceRel of Q ) by Def2;
( a = p1 & b = q1 & s = p2 & t = q2 ) by A1, A2, ZFMISC_1:33;
then ( r1 (--) r2 or q1 (--) q2 ) by A3, Def7;
hence ( not p1 (--) p2 or q1 (--) q2 ) by Th34; :: thesis: verum