let x be Surreal; :: thesis: ( x is No_ordinal implies ex A being Ordinal st x == No_uOrdinal_op A )
assume x is No_ordinal ; :: thesis: ex A being Ordinal st x == No_uOrdinal_op A
then consider A being Ordinal such that
A1: x == No_Ordinal_op A by Lm24;
No_Ordinal_op A == No_uOrdinal_op A by Th73;
then x == No_uOrdinal_op A by A1, SURREALO:4;
hence ex A being Ordinal st x == No_uOrdinal_op A ; :: thesis: verum