let r be Real; :: thesis: uReal . r in Day omega
( born_eq (sReal . r) c= born (sReal . r) & born (sReal . r) c= omega ) by SURREALO:def 5, SURREALN:49;
then A1: born_eq (sReal . r) c= omega by XBOOLE_1:1;
uReal . r = Unique_No (sReal . r) by SURREALN:def 7;
then ( born_eq (sReal . r) = born_eq (uReal . r) & born_eq (uReal . r) = born (uReal . r) ) by SURREALO:def 10, SURREALO:33, SURREALO:48;
then ( uReal . r in Day (born (uReal . r)) & Day (born (uReal . r)) c= Day omega ) by A1, SURREAL0:def 18, SURREAL0:35;
hence uReal . r in Day omega ; :: thesis: verum