let r be Real; :: thesis: ( born (uReal . r) = omega iff r is not Dyadic )
uReal . r = Unique_No (sReal . r) by Def7;
then A1: born_eq (sReal . r) = born_eq (uReal . r) by SURREALO:def 10, SURREALO:33;
A2: born_eq (uReal . r) = born (uReal . r) by SURREALO:48;
thus ( born (uReal . r) = omega implies not r is Dyadic ) :: thesis: ( r is not Dyadic implies born (uReal . r) = omega )

proof

assume A3: ( born (uReal . r) = omega & r is Dyadic ) ; :: thesis: contradiction
then reconsider r = r as Dyadic ;
born (uDyadic . r) is finite by Th37;
hence contradiction by Th46, A3; :: thesis: verum

end;

assume that
A4: r is not Dyadic and
A5: born (uReal . r) <> omega ; :: thesis: contradiction
( born_eq (sReal . r) c= born (sReal . r) & born (sReal . r) c= omega ) by SURREALO:def 5, Th49;
then born_eq (uReal . r) c< omega by A1, A2, A5, XBOOLE_0:def 8, XBOOLE_1:1;
then born_eq (uReal . r) in omega by ORDINAL1:11;
then reconsider B = born_eq (uReal . r) as Nat ;
consider x being Surreal such that
A6: ( born x = B & uReal . r == x ) by SURREALO:def 5;
x in Day B by A6, SURREAL0:def 18;
then consider d being Dyadic such that
A7: ( x == uDyadic . d & uDyadic . d in Day B ) by Th35;
( uReal . r == uDyadic . d & uDyadic . d == uReal . d ) by A7, A6, SURREALO:4, Th46;
then ( r <= d & d <= r ) by SURREALO:4, Th51;
hence contradiction by XXREAL_0:1, A4; :: thesis: verum