let A be Ordinal; :: thesis: ( No_uOrdinal_op A == No_Ordinal_op A & born (No_uOrdinal_op A) = A )
A1: No_uOrdinal_op A == No_Ordinal_op A by SURREALO:def 10;
( born_eq (No_uOrdinal_op A) = born_eq (No_Ordinal_op A) & born_eq (No_Ordinal_op A) c= born (No_Ordinal_op A) & born (No_Ordinal_op A) = A ) by SURREALO:33, SURREALO:def 5, SURREALO:def 10, Th70;
then A2: born (No_uOrdinal_op A) c= A by SURREALO:48;
A c= born (No_uOrdinal_op A)

proof

set B = born (No_uOrdinal_op A);
assume not A c= born (No_uOrdinal_op A) ; :: thesis: contradiction
then A3: No_Ordinal_op (born (No_uOrdinal_op A)) < No_Ordinal_op A by Th68, ORDINAL1:16;
No_uOrdinal_op A in Day (born (No_uOrdinal_op A)) by SURREAL0:def 18;
then No_uOrdinal_op A <= No_Ordinal_op (born (No_uOrdinal_op A)) by Th69;
hence contradiction by A1, A3, SURREALO:4; :: thesis: verum

end;

hence ( No_uOrdinal_op A == No_Ordinal_op A & born (No_uOrdinal_op A) = A ) by SURREALO:def 10, A2, XBOOLE_0:def 10; :: thesis: verum