let P, Q be non empty 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] & ( not p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
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] & ( not p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
let p1, p2 be Element of P; :: thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( not p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
let q1, q2 be Element of Q; :: thesis: ( p = [p1,q1] & q = [p2,q2] & ( not p1 (--) p2 or q1 (--) q2 ) implies p (--) q )
assume that
A1: p = [p1,q1] and
A2: q = [p2,q2] ; :: thesis: ( ( p1 (--) p2 & not q1 (--) q2 ) or p (--) q )
reconsider r1 = p1, r2 = p2 as Element of (pcs-reverse P) by Def40;
reconsider w1 = [r1,q1], w2 = [r2,q2] as Element of ((pcs-reverse P) pcs-times Q) by A1, A2;
assume ( not p1 (--) p2 or q1 (--) q2 ) ; :: thesis: p (--) q
then ( r1 (--) r2 or q1 (--) q2 ) by Th35;
then w1 (--) w2 by Th38;
hence p (--) q by A1, A2; :: thesis: verum