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