let P, Q be pcs-Str ; 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] holds
( p <= q iff ( p2 <= p1 & q1 <= q2 ) )
let p, q be 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] holds
( p <= q iff ( p2 <= p1 & q1 <= q2 ) )
let p1, p2 be Element of P; for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds
( p <= q iff ( p2 <= p1 & q1 <= q2 ) )
let q1, q2 be Element of Q; ( p = [p1,q1] & q = [p2,q2] implies ( p <= q iff ( p2 <= p1 & q1 <= q2 ) ) )
assume that
A1:
p = [p1,q1]
and
A2:
q = [p2,q2]
; ( p <= q iff ( p2 <= p1 & q1 <= q2 ) )
reconsider r1 = p1, r2 = p2 as Element of (pcs-reverse P) by Def40;
thus
( p <= q implies ( p2 <= p1 & q1 <= q2 ) )
( p2 <= p1 & q1 <= q2 implies p <= q )proof
assume
p <= q
;
( p2 <= p1 & q1 <= q2 )
then
[p,q] in [" the InternalRel of (pcs-reverse P), the InternalRel of Q"]
;
then consider a,
b,
s,
t being
object such that A3:
p = [a,b]
and A4:
q = [s,t]
and A5:
[a,s] in the
InternalRel of
(pcs-reverse P)
and A6:
[b,t] in the
InternalRel of
Q
by YELLOW_3:def 1;
A7:
a = p1
by A1, A3, XTUPLE_0:1;
A8:
b = q1
by A1, A3, XTUPLE_0:1;
s = p2
by A2, A4, XTUPLE_0:1;
then
r1 <= r2
by A5, A7;
hence
p2 <= p1
by Th33;
q1 <= q2
thus
[q1,q2] in the
InternalRel of
Q
by A2, A4, A6, A8, XTUPLE_0:1;
ORDERS_2:def 5 verum
end;
assume that
A9:
p2 <= p1
and
A10:
q1 <= q2
; p <= q
r1 <= r2
by A9, Th33;
then A11:
[r1,r2] in the InternalRel of (pcs-reverse P)
;
[q1,q2] in the InternalRel of Q
by A10;
hence
[p,q] in the InternalRel of (P --> Q)
by A1, A2, A11, YELLOW_3:def 1; ORDERS_2:def 5 verum