let A be Ordinal; :: thesis: No_uOrdinal_op A in Day A
born (No_uOrdinal_op A) = A by Th73;
hence No_uOrdinal_op A in Day A by SURREAL0:def 18; :: thesis: verum