let S1, S2 be non empty RelStr ; for a, c being Element of S1
for b, d being Element of S2 holds
( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
let a, c be Element of S1; for b, d being Element of S2 holds
( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
let b, d be Element of S2; ( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
set I1 = the InternalRel of S1;
set I2 = the InternalRel of S2;
set x = [[a,b],[c,d]];
A1:
( ([[a,b],[c,d]] `1) `1 = a & ([[a,b],[c,d]] `2) `1 = c )
;
A2:
( ([[a,b],[c,d]] `1) `2 = b & ([[a,b],[c,d]] `2) `2 = d )
;
thus
( a <= c & b <= d implies [a,b] <= [c,d] )
( [a,b] <= [c,d] implies ( a <= c & b <= d ) )proof
assume
(
a <= c &
b <= d )
;
[a,b] <= [c,d]
then
(
[(([[a,b],[c,d]] `1) `1),(([[a,b],[c,d]] `2) `1)] in the
InternalRel of
S1 &
[(([[a,b],[c,d]] `1) `2),(([[a,b],[c,d]] `2) `2)] in the
InternalRel of
S2 )
;
then
[[a,b],[c,d]] in [" the InternalRel of S1, the InternalRel of S2"]
by Th10;
hence
[[a,b],[c,d]] in the
InternalRel of
[:S1,S2:]
by Def2;
ORDERS_2:def 5 verum
end;
assume
[a,b] <= [c,d]
; ( a <= c & b <= d )
then
[[a,b],[c,d]] in the InternalRel of [:S1,S2:]
;
then
[[a,b],[c,d]] in [" the InternalRel of S1, the InternalRel of S2"]
by Def2;
hence
( [a,c] in the InternalRel of S1 & [b,d] in the InternalRel of S2 )
by A1, A2, Th10; ORDERS_2:def 5 verum