let x be Surreal; :: thesis: x <= x
defpred S₁[ Ordinal] means for x being Surreal st x in Day $1 holds
x <= 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: ( x in Day D implies x <= x )
assume A3: x in Day D ; :: thesis: x <= x
A4: x = [(L_ x),(R_ x)] ;
assume not x <= x ; :: thesis: contradiction

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

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

then consider xl, r being Surreal such that
A5: ( xl in L_ x & r in {x} & r <= xl ) ;
xl in (L_ x) \/ (R_ x) by A5, XBOOLE_0:def 3;
then consider O being Ordinal such that
A6: ( O in D & xl in Day O ) by A4, A3, SURREAL0:46;
x <= xl by A5, TARSKI:def 1;
then A7: L_ x << {xl} by SURREAL0:43;
xl in {xl} by TARSKI:def 1;
hence contradiction by A6, A2, A5, A7; :: thesis: verum

end;

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

then consider l, xr being Surreal such that
A8: ( l in {x} & xr in R_ x & xr <= l ) ;
xr in (L_ x) \/ (R_ x) by A8, XBOOLE_0:def 3;
then consider O being Ordinal such that
A9: ( O in D & xr in Day O ) by A4, A3, SURREAL0:46;
xr <= x by A8, TARSKI:def 1;
then A10: {xr} << R_ x by SURREAL0:43;
xr in {xr} by TARSKI:def 1;
hence contradiction by A9, A2, A8, A10; :: thesis: verum

end;

end;

end;

A11: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
ex A being Ordinal st x in Day A by SURREAL0:def 14;
hence x <= x by A11; :: thesis: verum