uReal . r = Unique_No (sReal . r) by Def7;
hence uReal . r is uniq-surreal ; :: thesis: verum