let r1, r2 be Real; :: thesis: ( uReal . r1 < uReal . r2 iff r1 < r2 )
( uReal . r1 = Unique_No (sReal . r1) & uReal . r2 = Unique_No (sReal . r2) ) by Def7;
then A1: ( uReal . r1 == sReal . r1 & uReal . r2 == sReal . r2 ) by SURREALO:def 10;
thus ( uReal . r1 < uReal . r2 implies r1 < r2 ) :: thesis: ( r1 < r2 implies uReal . r1 < uReal . r2 )

proof

assume uReal . r1 < uReal . r2 ; :: thesis: r1 < r2
then uReal . r1 < sReal . r2 by A1, SURREALO:4;
then sReal . r1 < sReal . r2 by A1, SURREALO:4;
hence r1 < r2 by Th50; :: thesis: verum

end;

assume r1 < r2 ; :: thesis: uReal . r1 < uReal . r2
then uReal . r1 < sReal . r2 by A1, SURREALO:4, Th50;
hence uReal . r1 < uReal . r2 by A1, SURREALO:4; :: thesis: verum