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