let S1, S2 be non empty RelStr ; :: thesis: 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; :: thesis: for b, d being Element of S2 holds
( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
let b, d be Element of S2; :: thesis: ( ( 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]] `1 ) `2 = b & ([[a,b],[c,d]] `2 ) `1 = c & ([[a,b],[c,d]] `2 ) `2 = d )
by Lm1;
A2:
( [[a,b],[c,d]] `1 = [a,b] & [[a,b],[c,d]] `2 = [c,d] )
by MCART_1:7;
thus
( a <= c & b <= d implies [a,b] <= [c,d] )
:: thesis: ( [a,b] <= [c,d] implies ( a <= c & b <= d ) )proof
assume
(
a <= c &
b <= d )
;
:: thesis: [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 )
by A1, ORDERS_2:def 9;
then
[[a,b],[c,d]] in ["the InternalRel of S1,the InternalRel of S2"]
by A2, Th10;
hence
[[a,b],[c,d]] in the
InternalRel of
[:S1,S2:]
by Def2;
:: according to ORDERS_2:def 9 :: thesis: verum
end;
assume
[a,b] <= [c,d]
; :: thesis: ( a <= c & b <= d )
then
[[a,b],[c,d]] in the InternalRel of [:S1,S2:]
by ORDERS_2:def 9;
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, Th10; :: according to ORDERS_2:def 9 :: thesis: verum