consider n being Nat such that
A1: ( - n < r & r < n ) by Lm22;
A2: ( sReal . n == uDyadic . n & uDyadic . n = uInt . n & sReal . (- n) == uDyadic . (- n) & uDyadic . (- n) = uInt . (- n) ) by Th46, Def5;
( uInt . (- n) < sReal . r & sReal . r < uInt . n ) by A1, Th50, A2, SURREALO:4;
hence sReal . r is *real by Lm21; :: thesis: verum