theorem Th50: :: SURREALN:50
for r1, r2 being Real holds
( sReal . r1 < sReal . r2 iff r1 < r2 )