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]] `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] ) :: 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 ) ;
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; :: according to ORDERS_2:def 5 :: thesis: verum

end;

assume [a,b] <= [c,d] ; :: thesis: ( 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; :: according to ORDERS_2:def 5 :: thesis: verum