theorem Th51: :: SURREALN:51

for r1, r2 being Real holds
( uReal . r1 < uReal . r2 iff r1 < r2 )