uReal . r = Unique_No (sReal . r) by Def7;
then uReal . r == sReal . r by SURREALO:def 10;
hence uReal . r is *real by Th61; :: thesis: verum