let A be Ordinal; :: thesis: ex x being No_ordinal Surreal st
( born x = A & No_uOrdinal_op A == x & ( for o being object holds
( o in L_ x iff ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) ) ) )
defpred S₁[ object ] means ex B being Ordinal st
( B in A & $1 = No_uOrdinal_op B );
consider X being set such that
A1: for o being object holds
( o in X iff ( o in Day A & S₁[o] ) ) from XBOOLE_0:sch 1();
A2: X << {} ;
for o being object st o in X \/ {} holds
ex O being Ordinal st
( O in A & o in Day O )

proof

let o be object ; :: thesis: ( o in X \/ {} implies ex O being Ordinal st
( O in A & o in Day O ) )
assume o in X \/ {} ; :: thesis: ex O being Ordinal st
( O in A & o in Day O )
then consider B being Ordinal such that
A3: ( B in A & o = No_uOrdinal_op B ) by A1;
born (No_uOrdinal_op B) = B by Th73;
then No_uOrdinal_op B in Day B by SURREAL0:def 18;
hence ex O being Ordinal st
( O in A & o in Day O ) by A3; :: thesis: verum

end;

then A4: [X,{}] in Day A by A2, SURREAL0:46;
then reconsider x = [X,{}] as Surreal ;
R_ x = {} ;
then reconsider x = x as No_ordinal Surreal by Def10;
take x ; :: thesis: ( born x = A & No_uOrdinal_op A == x & ( for o being object holds
( o in L_ x iff ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) ) ) )
for O being Ordinal st x in Day O holds
A c= O

proof

let O be Ordinal; :: thesis: ( x in Day O implies A c= O )
assume A5: ( x in Day O & not A c= O ) ; :: thesis: contradiction
A6: No_uOrdinal_op O in Day O by Th74;
Day O c= Day A by A5, SURREAL0:35;
then ( No_uOrdinal_op O in X & X = L_ x & L_ x << {x} & x in {x} ) by A6, A5, ORDINAL1:16, A1, SURREALO:11, TARSKI:def 1;
hence contradiction by A5, Th76; :: thesis: verum

end;

hence born x = A by A4, SURREAL0:def 18; :: thesis: ( No_uOrdinal_op A == x & ( for o being object holds
( o in L_ x iff ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) ) ) )
L_ (No_Ordinal_op A) << {x}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ (No_Ordinal_op A) or not b in {x} or not b <= a )
assume A7: ( a in L_ (No_Ordinal_op A) & b in {x} ) ; :: thesis: not b <= a
consider B being Ordinal such that
A8: ( B in A & a = No_Ordinal_op B ) by A7, Th71;
A9: ( No_uOrdinal_op B in Day B & Day B c= Day A ) by A8, ORDINAL1:def 2, Th74, SURREAL0:35;
( No_uOrdinal_op B in X & X = L_ x & L_ x << {x} ) by A8, A1, SURREALO:11, A9;
then ( a == No_uOrdinal_op B & No_uOrdinal_op B < b ) by A8, Th73, A7;
hence not b <= a by SURREALO:4; :: thesis: verum

end;

then A10: ( L_ (No_Ordinal_op A) << {x} & {(No_Ordinal_op A)} << R_ x ) ;
L_ x << {(No_Ordinal_op A)}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ x or not b in {(No_Ordinal_op A)} or not b <= a )
assume A11: ( a in L_ x & b in {(No_Ordinal_op A)} ) ; :: thesis: not b <= a
consider B being Ordinal such that
A12: ( B in A & a = No_uOrdinal_op B ) by A1, A11;
( a < No_uOrdinal_op A & No_uOrdinal_op A == No_Ordinal_op A ) by A12, Th75, Th73;
then a < No_Ordinal_op A by SURREALO:4;
hence not b <= a by A11, TARSKI:def 1; :: thesis: verum

end;

then ( L_ x << {(No_Ordinal_op A)} & {x} << R_ (No_Ordinal_op A) ) by Def10;
then ( No_uOrdinal_op A == No_Ordinal_op A & No_Ordinal_op A == x ) by SURREAL0:43, A10, Th73;
hence No_uOrdinal_op A == x by SURREALO:4; :: thesis: for o being object holds
( o in L_ x iff ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) )
let o be object ; :: thesis: ( o in L_ x iff ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) )
thus ( o in L_ x implies ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) ) by A1; :: thesis: ( ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) implies o in L_ x )
given B being Ordinal such that A13: ( B in A & o = No_uOrdinal_op B ) ; :: thesis: o in L_ x
( o in Day B & Day B c= Day A ) by A13, ORDINAL1:def 2, Th74, SURREAL0:35;
hence o in L_ x by A13, A1; :: thesis: verum