let A be Ordinal; :: thesis: born (No_Ordinal_op A) = A
A1: No_Ordinal_op A in Day A by Th67;
for O being Ordinal st No_Ordinal_op A in Day O holds
A c= O

proof

let O be Ordinal; :: thesis: ( No_Ordinal_op A in Day O implies A c= O )
assume A2: ( No_Ordinal_op A in Day O & not A c= O ) ; :: thesis: contradiction
No_Ordinal_op O < No_Ordinal_op A by Th68, A2, ORDINAL1:16;
hence contradiction by Th69, A2; :: thesis: verum

end;

hence born (No_Ordinal_op A) = A by A1, SURREAL0:def 18; :: thesis: verum