let x be Surreal; :: thesis: ( No_omega^ x is positive Surreal & ( for y1, y2, Ny1, Ny2 being Surreal st Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 holds
( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) ) )
defpred S₁[ Ordinal] means ( ( for x being Surreal st x in Day $1 holds
No_omega^ x is positive Surreal ) & ( for y1, y2, Ny1, Ny2 being Surreal st y1 in Day $1 & y2 in Day $1 & Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 holds
( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) ) );
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]
thus A3: for x being Surreal st x in Day D holds
No_omega^ x is positive Surreal :: thesis: for y1, y2, Ny1, Ny2 being Surreal st y1 in Day D & y2 in Day D & Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 holds
( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) )

proof

let x be Surreal; :: thesis: ( x in Day D implies No_omega^ x is positive Surreal )
assume A4: x in Day D ; :: thesis: No_omega^ x is positive Surreal
reconsider N = No_omega^ x as pair set by Lm4;
A5: born x c= D by A4, SURREAL0:def 18;
(L_ N) \/ (R_ N) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in (L_ N) \/ (R_ N) or o is surreal )
assume A6: o in (L_ N) \/ (R_ N) ; :: thesis: o is surreal

per cases ( o = 0_No or ( o <> 0_No & o in L_ N ) or o in R_ N ) by A6, XBOOLE_0:def 3;

suppose o = 0_No ; :: thesis: o is surreal

hence o is surreal ; :: thesis: verum

end;

suppose ( o <> 0_No & o in L_ N ) ; :: thesis: o is surreal

then ex a being Surreal ex r being positive Real st
( a in L_ x & o = (No_omega^ a) *' (uReal . r) ) by Lm4;
hence o is surreal ; :: thesis: verum

end;

suppose o in R_ N ; :: thesis: o is surreal

then ex a being Surreal ex r being positive Real st
( a in R_ x & o = (No_omega^ a) *' (uReal . r) ) by Lm4;
hence o is surreal ; :: thesis: verum

end;

end;

end;

then consider M being Ordinal such that
A7: for o being object st o in (L_ N) \/ (R_ N) holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
L_ N << R_ N

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ N or not b in R_ N or not b <= a )
assume A8: ( a in L_ N & b in R_ N ) ; :: thesis: not b <= a
consider xR being Surreal, r being positive Real such that
A9: ( xR in R_ x & b = (No_omega^ xR) *' (uReal . r) ) by A8, Lm4;
xR in (L_ x) \/ (R_ x) by A9, XBOOLE_0:def 3;
then A10: born xR in born x by SURREALO:1;
then A11: born xR in D by A5;
A12: xR in Day (born xR) by SURREAL0:def 18;
then reconsider NxR = No_omega^ xR as positive Surreal by A10, A2, A5;
A13: NxR * (uReal . r) is positive ;

per cases ( a = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & a = (No_omega^ xL) *' (uReal . r) ) ) by A8, Lm4;

suppose a = 0_No ; :: thesis: not b <= a

hence not b <= a by A13, A9; :: thesis: verum

end;

suppose ex xL being Surreal ex r being positive Real st
( xL in L_ x & a = (No_omega^ xL) *' (uReal . r) ) ; :: thesis: not b <= a

then consider xL being Surreal, s being positive Real such that
A14: ( xL in L_ x & a = (No_omega^ xL) *' (uReal . s) ) ;
xL in (L_ x) \/ (R_ x) by A14, XBOOLE_0:def 3;
then A15: born xL in born x by SURREALO:1;
then A16: born xL in D by A5;
set B = (born xL) \/ (born xR);
A17: (born xL) \/ (born xR) in D by A11, A16, ORDINAL3:12;
A18: xL in Day (born xL) by SURREAL0:def 18;
then reconsider NxL = No_omega^ xL as positive Surreal by A15, A5, A2;
A19: ( Day (born xL) c= Day ((born xL) \/ (born xR)) & Day (born xR) c= Day ((born xL) \/ (born xR)) ) by XBOOLE_1:7, SURREAL0:35;
L_ x << R_ x by SURREAL0:45;
then xL < xR by A14, A9;
then NxL infinitely< NxR by A17, A19, A18, A12, A2;
then NxL infinitely< NxR * (uReal . r) by Th13;
then NxL * (uReal . s) < NxR * (uReal . r) ;
hence not b <= a by A14, A9; :: thesis: verum

end;

end;

end;

then [(L_ N),(R_ N)] in Day M by A7, SURREAL0:46;
then reconsider N = N as Surreal ;
A20: 0_No in L_ N by Lm4;
( L_ N << {N} & N in {N} ) by SURREALO:11, TARSKI:def 1;
hence No_omega^ x is positive Surreal by A20, SURREALI:def 8; :: thesis: verum

end;

defpred S₂[ Ordinal] means for y1, y2, Ny1, Ny2 being Surreal st (born y1) (+) (born y2) = $1 & y1 in Day D & y2 in Day D & Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 holds
( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) );
A21: for E being Ordinal st ( for F being Ordinal st F in E holds
S₂[F] ) holds
S₂[E]

proof

let E be Ordinal; :: thesis: ( ( for F being Ordinal st F in E holds
S₂[F] ) implies S₂[E] )
assume A22: for F being Ordinal st F in E holds
S₂[F] ; :: thesis: S₂[E]
let y1, y2, Ny1, Ny2 be Surreal; :: thesis: ( (born y1) (+) (born y2) = E & y1 in Day D & y2 in Day D & Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 implies ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) )
assume A23: ( (born y1) (+) (born y2) = E & y1 in Day D & y2 in Day D & Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 ) ; :: thesis: ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) )
thus ( y1 <= y2 implies Ny1 <= Ny2 ) :: thesis: ( y1 < y2 implies Ny1 infinitely< Ny2 )

proof

assume y1 <= y2 ; :: thesis: Ny1 <= Ny2
then A24: ( L_ y1 << {y2} & {y1} << R_ y2 ) by SURREAL0:43;
A25: L_ Ny1 << {Ny2}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ Ny1 or not b in {Ny2} or not b <= a )
assume A26: ( a in L_ Ny1 & b in {Ny2} ) ; :: thesis: not b <= a

per cases ( a = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ y1 & a = (No_omega^ xL) *' (uReal . r) ) ) by A26, Lm4, A23;

suppose A27: a = 0_No ; :: thesis: not b <= a

Ny2 is positive by A3, A23;
hence not b <= a by A27, A26, TARSKI:def 1; :: thesis: verum

end;

suppose ex xL being Surreal ex r being positive Real st
( xL in L_ y1 & a = (No_omega^ xL) *' (uReal . r) ) ; :: thesis: not b <= a

then consider xL being Surreal, r being positive Real such that
A28: ( xL in L_ y1 & a = (No_omega^ xL) *' (uReal . r) ) ;
A29: xL in (L_ y1) \/ (R_ y1) by A28, XBOOLE_0:def 3;
then ( born xL c= born y1 & born y1 c= D ) by SURREALO:1, SURREAL0:def 18, ORDINAL1:def 2, A23;
then born xL c= D by XBOOLE_1:1;
then A30: ( xL in Day (born xL) & Day (born xL) c= Day D ) by SURREAL0:def 18, SURREAL0:35;
then reconsider NxL = No_omega^ xL as positive Surreal by A3;
y2 in {y2} by TARSKI:def 1;
then A31: xL < y2 by A24, A28;
(born xL) (+) (born y2) in E by A29, SURREALO:1, A23, ORDINAL7:94;
then NxL infinitely< Ny2 by A23, A30, A31, A22;
then NxL * (uReal . r) < Ny2 ;
hence not b <= a by A28, A26, TARSKI:def 1; :: thesis: verum

end;

end;

end;

{Ny1} << R_ Ny2

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in {Ny1} or not b in R_ Ny2 or not b <= a )
assume A32: ( a in {Ny1} & b in R_ Ny2 ) ; :: thesis: not b <= a
consider xR being Surreal, r being positive Real such that
A33: ( xR in R_ y2 & b = (No_omega^ xR) *' (uReal . r) ) by A23, A32, Lm4;
A34: xR in (L_ y2) \/ (R_ y2) by A33, XBOOLE_0:def 3;
then ( born xR c= born y2 & born y2 c= D ) by SURREALO:1, SURREAL0:def 18, ORDINAL1:def 2, A23;
then born xR c= D by XBOOLE_1:1;
then A35: ( xR in Day (born xR) & Day (born xR) c= Day D ) by SURREAL0:def 18, SURREAL0:35;
then reconsider NxR = No_omega^ xR as positive Surreal by A3;
y1 in {y1} by TARSKI:def 1;
then A36: y1 < xR by A24, A33;
(born y1) (+) (born xR) in E by A34, SURREALO:1, A23, ORDINAL7:94;
then Ny1 infinitely< NxR by A23, A35, A36, A22;
then Ny1 infinitely< NxR * (uReal . r) by Th13;
then Ny1 * (uReal . 1) < NxR * (uReal . r) ;
hence not b <= a by A33, SURREALN:48, A32, TARSKI:def 1; :: thesis: verum

end;

hence Ny1 <= Ny2 by A25, SURREAL0:43; :: thesis: verum

end;

assume A37: y1 < y2 ; :: thesis: Ny1 infinitely< Ny2
let r be positive Real; :: according to SURREALC:def 3 :: thesis: Ny1 * (uReal . r) < Ny2
A38: ( born y1 c= D & born y2 c= D ) by A23, SURREAL0:def 18;

per cases ( ex y1R being Surreal st
( y1R in R_ y1 & y1 < y1R & y1R <= y2 ) or ex y2L being Surreal st
( y2L in L_ y2 & y1 <= y2L & y2L < y2 ) ) by A37, SURREALO:13;

suppose ex y1R being Surreal st
( y1R in R_ y1 & y1 < y1R & y1R <= y2 ) ; :: thesis: Ny1 * (uReal . r) < Ny2

then consider y1R being Surreal such that
A39: ( y1R in R_ y1 & y1 < y1R & y1R <= y2 ) ;
A40: y1R in (L_ y1) \/ (R_ y1) by A39, XBOOLE_0:def 3;
then A41: born y1R in born y1 by SURREALO:1;
y1R in Day (born y1R) by SURREAL0:def 18;
then reconsider Ny1R = No_omega^ y1R as positive Surreal by A41, A38, A2;
A42: ( Ny1 in {Ny1} & {Ny1} << R_ Ny1 ) by TARSKI:def 1, SURREALO:11;
A43: Ny1 < Ny1R * (uReal . (1 / r)) by A42, A39, A23, Lm4;
uReal . r is positive ;
then A44: Ny1 * (uReal . r) < (Ny1R * (uReal . (1 / r))) * (uReal . r) by A43, SURREALR:70;
(1 / r) * r = 1 by XCMPLX_1:106;
then ( (Ny1R * (uReal . (1 / r))) * (uReal . r) == Ny1R * ((uReal . (1 / r)) * (uReal . r)) & Ny1R * ((uReal . (1 / r)) * (uReal . r)) == Ny1R * 1_No ) by SURREALR:51, SURREALR:69, SURREALN:48, SURREALN:57;
then ( (Ny1R * (uReal . (1 / r))) * (uReal . r) == Ny1R * 1_No & Ny1R * 1_No = Ny1R ) by SURREALO:4;
then A45: Ny1 * (uReal . r) < Ny1R by A44, SURREALO:4;
( born y1R c= born y1 & born y1 c= D ) by ORDINAL1:def 2, SURREAL0:def 18, SURREALO:1, A23, A40;
then born y1R c= D by XBOOLE_1:1;
then A46: ( y1R in Day (born y1R) & Day (born y1R) c= Day D ) by SURREAL0:def 18, SURREAL0:35;
(born y1R) (+) (born y2) in (born y1) (+) (born y2) by A40, SURREALO:1, ORDINAL7:94;
then Ny1R <= Ny2 by A39, A46, A23, A22;
hence Ny1 * (uReal . r) < Ny2 by A45, SURREALO:4; :: thesis: verum

end;

suppose ex y2L being Surreal st
( y2L in L_ y2 & y1 <= y2L & y2L < y2 ) ; :: thesis: Ny1 * (uReal . r) < Ny2

then consider y2L being Surreal such that
A47: ( y2L in L_ y2 & y1 <= y2L & y2L < y2 ) ;
A48: y2L in (L_ y2) \/ (R_ y2) by A47, XBOOLE_0:def 3;
then A49: born y2L in born y2 by SURREALO:1;
y2L in Day (born y2L) by SURREAL0:def 18;
then reconsider Ny2L = No_omega^ y2L as positive Surreal by A49, A38, A2;
A50: ( L_ Ny2 << {Ny2} & Ny2 in {Ny2} ) by TARSKI:def 1, SURREALO:11;
A51: Ny2L * (uReal . r) in L_ Ny2 by A47, A23, Lm4;
( born y2L c= born y2 & born y2 c= D ) by ORDINAL1:def 2, SURREAL0:def 18, SURREALO:1, A23, A48;
then born y2L c= D by XBOOLE_1:1;
then A52: ( y2L in Day (born y2L) & Day (born y2L) c= Day D ) by SURREAL0:def 18, SURREAL0:35;
(born y1) (+) (born y2L) in (born y1) (+) (born y2) by A48, SURREALO:1, ORDINAL7:94;
then A53: Ny1 <= Ny2L by A52, A47, A23, A22;
uReal . r is positive ;
then 0_No <= uReal . r ;
then Ny1 * (uReal . r) <= Ny2L * (uReal . r) by SURREALR:75, A53;
hence Ny1 * (uReal . r) < Ny2 by A51, A50, SURREALO:4; :: thesis: verum

end;

end;

end;

A54: for E being Ordinal holds S₂[E] from ORDINAL1:sch 2(A21);
let y1, y2, Ny1, Ny2 be Surreal; :: thesis: ( y1 in Day D & y2 in Day D & Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 implies ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) )
assume A55: ( y1 in Day D & y2 in Day D & Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 ) ; :: thesis: ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) )
S₂[(born y1) (+) (born y2)] by A54;
hence ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) by A55; :: thesis: verum

end;

A56: for E being Ordinal holds S₁[E] from ORDINAL1:sch 2(A1);
x in Day (born x) by SURREAL0:def 18;
hence No_omega^ x is positive Surreal by A56; :: thesis: for y1, y2, Ny1, Ny2 being Surreal st Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 holds
( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) )
let y1, y2, Ny1, Ny2 be Surreal; :: thesis: ( Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 implies ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) )
assume A57: ( Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 ) ; :: thesis: ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) )
A58: ( y1 in Day (born y1) & y2 in Day (born y2) ) by SURREAL0:def 18;
( Day (born y1) c= Day ((born y1) \/ (born y2)) & Day (born y2) c= Day ((born y1) \/ (born y2)) ) by XBOOLE_1:7, SURREAL0:35;
hence ( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) by A57, A58, A56; :: thesis: verum