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] holds
( p <= q iff ( p2 <= p1 & 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] holds
( p <= q iff ( p2 <= p1 & q1 <= q2 ) )
let p1, p2 be Element of P; :: thesis: 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; :: thesis: ( p = [p1,q1] & q = [p2,q2] implies ( p <= q iff ( p2 <= p1 & q1 <= q2 ) ) )
assume A1:
( p = [p1,q1] & q = [p2,q2] )
; :: thesis: ( 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 ) )
:: thesis: ( p2 <= p1 & q1 <= q2 implies p <= q )proof
assume
p <= q
;
:: thesis: ( p2 <= p1 & q1 <= q2 )
then
[p,q] in ["the InternalRel of (pcs-reverse P),the InternalRel of Q"]
by ORDERS_2:def 9;
then consider a,
b,
s,
t being
set such that A2:
(
p = [a,b] &
q = [s,t] )
and A3:
[a,s] in the
InternalRel of
(pcs-reverse P)
and A4:
[b,t] in the
InternalRel of
Q
by YELLOW_3:def 1;
A5:
(
a = p1 &
b = q1 &
s = p2 &
t = q2 )
by A1, A2, ZFMISC_1:33;
then
r1 <= r2
by A3, ORDERS_2:def 9;
hence
p2 <= p1
by Th33;
:: thesis: q1 <= q2
thus
[q1,q2] in the
InternalRel of
Q
by A4, A5;
:: according to ORDERS_2:def 9 :: thesis: verum
end;
assume
( p2 <= p1 & q1 <= q2 )
; :: thesis: p <= q
then
( r1 <= r2 & q1 <= q2 )
by Th33;
then
( [r1,r2] in the InternalRel of (pcs-reverse P) & [q1,q2] in the InternalRel of Q )
by ORDERS_2:def 9;
hence
[p,q] in the InternalRel of (P --> Q)
by A1, YELLOW_3:def 1; :: according to ORDERS_2:def 9 :: thesis: verum