let c, x be uSurreal; :: thesis: ( L_ c << {x} & {x} << R_ c & x <> c implies born c in born x )
assume that
A1: ( L_ c << {x} & {x} << R_ c & x <> c ) and
A2: not born c in born x ; :: thesis: contradiction
A3: born c = born_eq c by Th48;
then ( born c c= born x & born x c= born c ) by A1, A2, Th51, ORDINAL1:16;
then A4: born c = born x by XBOOLE_0:def 10;
not x == c by A1, Th50;

per cases then ( x < c or c < x ) ;

suppose x < c ; :: thesis: contradiction

per cases then ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= c ) or ex cL being Surreal st
( cL in L_ c & x <= cL & cL < c ) ) by Th13;

suppose ex xR being Surreal st
( xR in R_ x & x < xR & xR <= c ) ; :: thesis: contradiction

then consider xR being Surreal such that
A5: ( xR in R_ x & x < xR & xR <= c ) ;
xR in (L_ x) \/ (R_ x) by A5, XBOOLE_0:def 3;
then A6: born xR in born x by Th1;
( {c} << R_ c & x <= xR ) by A5, Th11;
then ( L_ c << {xR} & {xR} << R_ c ) by A1, A5, Th17, Th18;
then born c in born x by A3, Th51, A6, ORDINAL1:12;
hence contradiction by A4; :: thesis: verum

end;

suppose ex cL being Surreal st
( cL in L_ c & x <= cL & cL < c ) ; :: thesis: contradiction

then consider cL being Surreal such that
A7: ( cL in L_ c & x <= cL & cL < c ) ;
( L_ c << {cL} & cL in {cL} ) by A1, TARSKI:def 1, A7, Th17;
hence contradiction by A7, Th3; :: thesis: verum

end;

end;

end;

suppose c < x ; :: thesis: contradiction

per cases then ( ex cR being Surreal st
( cR in R_ c & c < cR & cR <= x ) or ex xL being Surreal st
( xL in L_ x & c <= xL & xL < x ) ) by Th13;

suppose ex cR being Surreal st
( cR in R_ c & c < cR & cR <= x ) ; :: thesis: contradiction

then consider cR being Surreal such that
A8: ( cR in R_ c & c < cR & cR <= x ) ;
( cR in {cR} & {cR} << R_ c ) by A1, A8, Th18, TARSKI:def 1;
hence contradiction by A8, Th3; :: thesis: verum

end;

suppose ex xL being Surreal st
( xL in L_ x & c <= xL & xL < x ) ; :: thesis: contradiction

then consider xL being Surreal such that
A9: ( xL in L_ x & c <= xL & xL < x ) ;
xL in (L_ x) \/ (R_ x) by A9, XBOOLE_0:def 3;
then A10: born xL in born x by Th1;
( L_ c << {c} & xL <= x ) by A9, Th11;
then ( L_ c << {xL} & {xL} << R_ c ) by A1, A9, Th17, Th18;
then born c in born x by A3, Th51, A10, ORDINAL1:12;
hence contradiction by A4; :: thesis: verum

end;

end;

end;

end;