defpred S₁[ Ordinal] means for x being Surreal st born x c= $1 holds
( L_ x <<= {x} & {x} <<= R_ x );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let x be Surreal; :: thesis: ( born x c= D implies ( L_ x <<= {x} & {x} <<= R_ x ) )
assume A3: born x c= D ; :: thesis: ( L_ x <<= {x} & {x} <<= R_ x )

per cases ( born x in D or born x = D ) by A3, ORDINAL1:11, XBOOLE_0:def 8;

suppose born x in D ; :: thesis: ( L_ x <<= {x} & {x} <<= R_ x )

hence ( L_ x <<= {x} & {x} <<= R_ x ) by A2; :: thesis: verum

end;

suppose A4: born x = D ; :: thesis: ( L_ x <<= {x} & {x} <<= R_ x )

thus L_ x <<= {x} :: thesis: {x} <<= R_ x

proof

given r, xl being Surreal such that A5: ( r in {x} & xl in L_ x & not xl <= r ) ; :: according to SURREAL0:def 19 :: thesis: contradiction
not xl <= x by A5, TARSKI:def 1;

per cases then ( not L_ xl << {x} or not {xl} << R_ x ) by SURREAL0:43;

suppose not L_ xl << {x} ; :: thesis: contradiction

then consider xll, X being Surreal such that
A6: ( xll in L_ xl & X in {x} & X <= xll ) ;
A7: x <= xll by A6, TARSKI:def 1;
A8: xl in {xl} by TARSKI:def 1;
xl in (L_ x) \/ (R_ x) by A5, XBOOLE_0:def 3;
then born xl in D by A4, Th1;
then L_ xl <<= {xl} by A2;
then xll <= xl by A8, A6;
then x <= xl by A7, Th4;
then L_ x << {xl} by SURREAL0:43;
hence contradiction by Th3, A5, A8; :: thesis: verum

end;

suppose not {xl} << R_ x ; :: thesis: contradiction

then consider X, xr being Surreal such that
A9: ( X in {xl} & xr in R_ x & xr <= X ) ;
A10: L_ x << R_ x by SURREAL0:45;
xr <= xl by A9, TARSKI:def 1;
hence contradiction by A10, A9, A5; :: thesis: verum

end;

end;

end;

thus {x} <<= R_ x :: thesis: verum

proof

given xr, l being Surreal such that A11: ( xr in R_ x & l in {x} & not l <= xr ) ; :: according to SURREAL0:def 19 :: thesis: contradiction
not x <= xr by A11, TARSKI:def 1;

per cases then ( not {x} << R_ xr or not L_ x << {xr} ) by SURREAL0:43;

suppose not {x} << R_ xr ; :: thesis: contradiction

then consider X, xrr being Surreal such that
A12: ( X in {x} & xrr in R_ xr & xrr <= X ) ;
A13: xrr <= x by A12, TARSKI:def 1;
A14: xr in {xr} by TARSKI:def 1;
xr in (L_ x) \/ (R_ x) by A11, XBOOLE_0:def 3;
then born xr in D by A4, Th1;
then {xr} <<= R_ xr by A2;
then xr <= xrr by A14, A12;
then xr <= x by A13, Th4;
then {xr} << R_ x by SURREAL0:43;
hence contradiction by A11, A14, Th3; :: thesis: verum

end;

suppose not L_ x << {xr} ; :: thesis: contradiction

then consider xl, X being Surreal such that
A15: ( xl in L_ x & X in {xr} & X <= xl ) ;
A16: L_ x << R_ x by SURREAL0:45;
xr <= xl by A15, TARSKI:def 1;
hence contradiction by A16, A15, A11; :: thesis: verum

end;

end;

end;

end;

end;

end;

A17: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
let x be Surreal; :: thesis: ( L_ x <<= {x} & {x} <<= R_ x )
S₁[ born x] by A17;
hence ( L_ x <<= {x} & {x} <<= R_ x ) ; :: thesis: verum