let r1, r2 be Real; :: thesis: ( sReal . r1 < sReal . r2 iff r1 < r2 )
set R1 = sReal . r1;
set R2 = sReal . r2;
A1: ( L_ (sReal . r1) << {(sReal . r1)} & {(sReal . r1)} << R_ (sReal . r1) & sReal . r1 in {(sReal . r1)} & L_ (sReal . r2) << {(sReal . r2)} & {(sReal . r2)} << R_ (sReal . r2) & sReal . r2 in {(sReal . r2)} ) by SURREALO:11, TARSKI:def 1;
thus ( sReal . r1 < sReal . r2 implies r1 < r2 ) :: thesis: ( r1 < r2 implies sReal . r1 < sReal . r2 )

proof

assume A2: sReal . r1 < sReal . r2 ; :: thesis: r1 < r2
then A3: r1 <> r2 by SURREALO:3;
assume not r1 < r2 ; :: thesis: contradiction
then r2 < r1 by A3, XXREAL_0:1;
then 0 < r1 - r2 by XREAL_1:50;
then consider k being Nat such that
A4: 1 / (2 |^ k) <= r1 - r2 by PREPOWER:92;
set K2 = 2 |^ (k + 1);
2 |^ (k + 1) = 2 * (2 |^ k) by NEWTON:6;
then A5: (2 |^ (k + 1)) * (1 / (2 |^ k)) = 2 * ((2 |^ k) * (1 / (2 |^ k)))
.= 2 * 1 by XCMPLX_1:106 ;
A6: (2 |^ (k + 1)) * (r2 + (1 / (2 |^ k))) <= r1 * (2 |^ (k + 1)) by A4, XREAL_1:19, XREAL_1:64;
A7: uDyadic . ([/((r1 * (2 |^ (k + 1))) - 1)\] / (2 |^ (k + 1))) <= sReal . r1 by A1, Th42;
sReal . r2 <= uDyadic . ([\((r2 * (2 |^ (k + 1))) + 1)/] / (2 |^ (k + 1))) by A1, Th43;
then sReal . r1 < uDyadic . ([\((r2 * (2 |^ (k + 1))) + 1)/] / (2 |^ (k + 1))) by A2, SURREALO:4;
then uDyadic . ([/((r1 * (2 |^ (k + 1))) - 1)\] / (2 |^ (k + 1))) < uDyadic . ([\((r2 * (2 |^ (k + 1))) + 1)/] / (2 |^ (k + 1))) by A7, SURREALO:4;
then ( (r1 * (2 |^ (k + 1))) - 1 <= [/((r1 * (2 |^ (k + 1))) - 1)\] & [/((r1 * (2 |^ (k + 1))) - 1)\] < [\((r2 * (2 |^ (k + 1))) + 1)/] ) by Th24, XREAL_1:72, INT_1:def 7;
then ( (r1 * (2 |^ (k + 1))) - 1 < [\((r2 * (2 |^ (k + 1))) + 1)/] & [\((r2 * (2 |^ (k + 1))) + 1)/] <= (r2 * (2 |^ (k + 1))) + 1 ) by XXREAL_0:2, INT_1:def 6;
then (r1 * (2 |^ (k + 1))) - 1 < (r2 * (2 |^ (k + 1))) + 1 by XXREAL_0:2;
then ( ((r1 * (2 |^ (k + 1))) - 1) + 1 < ((r2 * (2 |^ (k + 1))) + 1) + 1 & ((r2 * (2 |^ (k + 1))) + 1) + 1 = (r2 * (2 |^ (k + 1))) + 2 ) by XREAL_1:6;
hence contradiction by A6, A5; :: thesis: verum

end;

assume r1 < r2 ; :: thesis: sReal . r1 < sReal . r2
then 0 < r2 - r1 by XREAL_1:50;
then consider k being Nat such that
A8: 1 / (2 |^ k) <= r2 - r1 by PREPOWER:92;
set K2 = 2 |^ (k + 1);
2 |^ (k + 1) = 2 * (2 |^ k) by NEWTON:6;
then A9: (2 |^ (k + 1)) * (1 / (2 |^ k)) = 2 * ((2 |^ k) * (1 / (2 |^ k)))
.= 2 * 1 by XCMPLX_1:106 ;
(2 |^ (k + 1)) * (r1 + (1 / (2 |^ k))) <= r2 * (2 |^ (k + 1)) by A8, XREAL_1:19, XREAL_1:64;
then (((2 |^ (k + 1)) * r1) + 2) - 1 <= (r2 * (2 |^ (k + 1))) - 1 by A9, XREAL_1:9;
then ( [\(((2 |^ (k + 1)) * r1) + 1)/] <= ((2 |^ (k + 1)) * r1) + 1 & ((2 |^ (k + 1)) * r1) + 1 <= (r2 * (2 |^ (k + 1))) - 1 ) by INT_1:def 6;
then ( [\(((2 |^ (k + 1)) * r1) + 1)/] <= (r2 * (2 |^ (k + 1))) - 1 & (r2 * (2 |^ (k + 1))) - 1 <= [/((r2 * (2 |^ (k + 1))) - 1)\] ) by XXREAL_0:2, INT_1:def 7;
then [\(((2 |^ (k + 1)) * r1) + 1)/] <= [/((r2 * (2 |^ (k + 1))) - 1)\] by XXREAL_0:2;
then A10: uDyadic . ([\(((2 |^ (k + 1)) * r1) + 1)/] / (2 |^ (k + 1))) <= uDyadic . ([/((r2 * (2 |^ (k + 1))) - 1)\] / (2 |^ (k + 1))) by XREAL_1:72, Th24;
sReal . r1 < uDyadic . ([\(((2 |^ (k + 1)) * r1) + 1)/] / (2 |^ (k + 1))) by A1, Th43;
then A11: sReal . r1 < uDyadic . ([/((r2 * (2 |^ (k + 1))) - 1)\] / (2 |^ (k + 1))) by A10, SURREALO:4;
uDyadic . ([/((r2 * (2 |^ (k + 1))) - 1)\] / (2 |^ (k + 1))) <= sReal . r2 by A1, Th42;
hence sReal . r1 < sReal . r2 by A11, SURREALO:4; :: thesis: verum