let x, c be Surreal; :: thesis: ( born c = born_eq c & L_ c << {x} & {x} << R_ c implies born c c= born x )
assume that
A1: ( born c = born_eq c & L_ c << {x} & {x} << R_ c ) and
A2: not born c c= born x ; :: thesis: contradiction
defpred S₁[ Ordinal] means ex y being Surreal st
( L_ c << {y} & {y} << R_ c & born y = $1 );
S₁[ born x] by A1;
then A3: ex A being Ordinal st S₁[A] ;
consider A being Ordinal such that
A4: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A3);
consider y being Surreal such that
A5: ( L_ c << {y} & {y} << R_ c & born y = A ) by A4;
( A c= born x & born x in born c ) by A1, A2, ORDINAL1:16, A4;
then A6: born y in born c by A5, ORDINAL1:12;
for z being Surreal st L_ c << {z} & {z} << R_ c holds
born y c= born z by A4, A5;
then born_eq c = born_eq y by A5, Th16, Th33;
hence contradiction by A1, ORDINAL1:5, A6, Def5; :: thesis: verum