let x be Surreal; :: thesis: ( x is No_ordinal implies ex A being Ordinal st x == No_Ordinal_op A )
defpred S₁[ Ordinal] means x <= No_Ordinal_op $1;
x in Day (born x) by SURREAL0:def 18;
then x <= No_Ordinal_op (born x) by Th69;
then A1: ex C being Ordinal st S₁[C] ;
consider Min being Ordinal such that
A2: ( S₁[Min] & ( for C being Ordinal st S₁[C] holds
Min c= C ) ) from ORDINAL1:sch 1(A1);
assume A3: x is No_ordinal ; :: thesis: ex A being Ordinal st x == No_Ordinal_op A
take Min ; :: thesis: x == No_Ordinal_op Min
set M = No_Ordinal_op Min;
L_ (No_Ordinal_op Min) << {x}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ (No_Ordinal_op Min) or not b in {x} or not b <= a )
assume A4: ( a in L_ (No_Ordinal_op Min) & b in {x} & not a < b ) ; :: thesis: contradiction
consider B being Ordinal such that
A5: ( B in Min & a = No_Ordinal_op B ) by A4, Th71;
S₁[B] by A5, A4, TARSKI:def 1;
hence contradiction by A2, A5, ORDINAL1:5; :: thesis: verum

end;

then ( L_ (No_Ordinal_op Min) << {x} & {(No_Ordinal_op Min)} << R_ x ) by A3;
hence x == No_Ordinal_op Min by A2, SURREAL0:43; :: thesis: verum