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