let x be Surreal; :: thesis: ( x is positive implies ex y being Surreal st x, No_omega^ y are_commensurate )
assume A1: x is positive ; :: thesis: ex y being Surreal st x, No_omega^ y are_commensurate
defpred S₁[ Ordinal] means for x being Surreal st x is positive & born x = $1 holds
ex y being Surreal st x, No_omega^ y are_commensurate ;
A2: 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 A3: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let x be Surreal; :: thesis: ( x is positive & born x = D implies ex y being Surreal st x, No_omega^ y are_commensurate )
assume A4: ( x is positive & born x = D ) ; :: thesis: ex y being Surreal st x, No_omega^ y are_commensurate
set X = ||.x.||;

per cases ( ex x1, y being Surreal st
( x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & x1, No_omega^ y are_commensurate & x, No_omega^ y are_commensurate ) or for x1, y being Surreal st x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & x1, No_omega^ y are_commensurate holds
not x, No_omega^ y are_commensurate ) ;

suppose ex x1, y being Surreal st
( x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & x1, No_omega^ y are_commensurate & x, No_omega^ y are_commensurate ) ; :: thesis: ex y being Surreal st x, No_omega^ y are_commensurate

then consider x1, y being Surreal such that
A5: ( x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & x1, No_omega^ y are_commensurate & x, No_omega^ y are_commensurate ) ;
take y ; :: thesis: x, No_omega^ y are_commensurate
thus x, No_omega^ y are_commensurate by A5; :: thesis: verum

end;

suppose A6: for x1, y being Surreal st x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & x1, No_omega^ y are_commensurate holds
not x, No_omega^ y are_commensurate ; :: thesis: ex y being Surreal st x, No_omega^ y are_commensurate

defpred S₂[ object , object ] means ( $2 is Surreal & ( for a, b being Surreal st a = $1 & $2 = b holds
a, No_omega^ b are_commensurate ) );
A7: for o being object st o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} holds
ex u being object st S₂[o,u]

proof

let o be object ; :: thesis: ( o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} implies ex u being object st S₂[o,u] )
assume A8: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis: ex u being object st S₂[o,u]
reconsider o = o as Surreal by A8, SURREAL0:def 16;
reconsider o = o as positive Surreal by A4, A8, SURREALI:21;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A4, SURREALI:20;
then born o in born x by A8, SURREALO:1;
then consider y being Surreal such that
A9: o, No_omega^ y are_commensurate by A3, A4;
take y ; :: thesis: S₂[o,y]
thus S₂[o,y] by A9; :: thesis: verum

end;

consider Y being Function such that
A10: ( dom Y = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & ( for o being object st o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} holds
S₂[o,Y . o] ) ) from CLASSES1:sch 1(A7);
set Y1 = Y .: ((L_ ||.x.||) \ {0_No});
set Y2 = Y .: ((R_ ||.x.||) \ {0_No});
dom Y = ((L_ ||.x.||) \ {0_No}) \/ ((R_ ||.x.||) \ {0_No}) by A10, XBOOLE_1:42;
then A11: ( rng Y = Y .: (dom Y) & Y .: (dom Y) = (Y .: ((L_ ||.x.||) \ {0_No})) \/ (Y .: ((R_ ||.x.||) \ {0_No})) ) by RELAT_1:113, RELAT_1:120;
rng Y is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in rng Y or o is surreal )
assume o in rng Y ; :: thesis: o is surreal
then ex a being object st
( a in dom Y & Y . a = o ) by FUNCT_1:def 3;
hence o is surreal by A10; :: thesis: verum

end;

then consider M being Ordinal such that
A12: for o being object st o in (Y .: ((L_ ||.x.||) \ {0_No})) \/ (Y .: ((R_ ||.x.||) \ {0_No})) holds
ex A being Ordinal st
( A in M & o in Day A ) by A11, SURREAL0:47;
A13: ( x in {x} & L_ x << {x} & {x} << R_ x ) by SURREALO:11, TARSKI:def 1;
Y .: ((L_ ||.x.||) \ {0_No}) << Y .: ((R_ ||.x.||) \ {0_No})

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in Y .: ((L_ ||.x.||) \ {0_No}) or not b in Y .: ((R_ ||.x.||) \ {0_No}) or not b <= a )
assume that
A14: ( a in Y .: ((L_ ||.x.||) \ {0_No}) & b in Y .: ((R_ ||.x.||) \ {0_No}) ) and
A15: not a < b ; :: thesis: contradiction
consider a1 being object such that
A16: ( a1 in dom Y & a1 in (L_ ||.x.||) \ {0_No} & a = Y . a1 ) by A14, FUNCT_1:def 6;
reconsider a1 = a1 as Surreal by SURREAL0:def 16, A16;
A17: a1, No_omega^ a are_commensurate by A16, A10;
( a1 in L_ ||.x.|| & a1 <> 0_No ) by A16, ZFMISC_1:56;
then a1 in L_ x by A4, SURREALI:def 9;
then A18: a1 <= x by A13;
not x, No_omega^ a are_commensurate by A6, A16, A10, A17;
then A19: No_omega^ a infinitely< x by Th29, A16, A10, A18;
consider b1 being object such that
A20: ( b1 in dom Y & b1 in (R_ ||.x.||) \ {0_No} & b = Y . b1 ) by A14, FUNCT_1:def 6;
reconsider b1 = b1 as Surreal by A20, SURREAL0:def 16;
A21: b1, No_omega^ b are_commensurate by A20, A10;
b1 in R_ x by A20, A4, SURREALI:def 9;
then A22: x <= b1 by A13;
not x, No_omega^ b are_commensurate by A6, A20, A10, A21;
then x infinitely< No_omega^ b by Th30, A20, A10, A4, A22;
then No_omega^ a < No_omega^ b by Th9, A19, Th14;
hence contradiction by A15, Lm5; :: thesis: verum

end;

then [(Y .: ((L_ ||.x.||) \ {0_No})),(Y .: ((R_ ||.x.||) \ {0_No}))] in Day M by A12, SURREAL0:46;
then reconsider YY = [(Y .: ((L_ ||.x.||) \ {0_No})),(Y .: ((R_ ||.x.||) \ {0_No}))] as Surreal ;
set N = No_omega^ YY;
A23: ( L_ (No_omega^ YY) << {(No_omega^ YY)} & {(No_omega^ YY)} << R_ (No_omega^ YY) & No_omega^ YY in {(No_omega^ YY)} ) by SURREALO:11, TARSKI:def 1;
A24: L_ ||.x.|| << {(No_omega^ YY)}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ ||.x.|| or not b in {(No_omega^ YY)} or not b <= a )
assume A25: ( a in L_ ||.x.|| & b in {(No_omega^ YY)} ) ; :: thesis: not b <= a
A26: b = No_omega^ YY by A25, TARSKI:def 1;
A27: a in (L_ ||.x.||) \/ (R_ ||.x.||) by A25, XBOOLE_0:def 3;

per cases ( a = 0_No or a <> 0_No ) ;

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

hence not b <= a by A26, SURREALI:def 8; :: thesis: verum

end;

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

then A28: ( a in (L_ ||.x.||) \ {0_No} & a in dom Y ) by A10, A27, A25, ZFMISC_1:56;
then A29: ( Y . a in Y .: ((L_ ||.x.||) \ {0_No}) & Y .: ((L_ ||.x.||) \ {0_No}) = YY `1 ) by FUNCT_1:def 6;
then reconsider Ya = Y . a as Surreal by SURREAL0:def 16;
a, No_omega^ Ya are_commensurate by A28, A10;
then consider n being positive Nat such that
A30: a < (No_omega^ Ya) * (uInt . n) ;
( uInt . n = uDyadic . n & uDyadic . n = uReal . n ) by SURREALN:46, SURREALN:def 5;
then A31: a <= (No_omega^ Ya) * (uReal . n) by A30;
(No_omega^ Ya) * (uReal . n) in L_ (No_omega^ YY) by Th22, A29;
hence not b <= a by A23, A25, A31, SURREALO:4; :: thesis: verum

end;

end;

end;

A32: {(No_omega^ YY)} << R_ ||.x.||

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not b in {(No_omega^ YY)} or not a in R_ ||.x.|| or not a <= b )
assume A33: ( b in {(No_omega^ YY)} & a in R_ ||.x.|| ) ; :: thesis: not a <= b
A34: b = No_omega^ YY by A33, TARSKI:def 1;
A35: a in (L_ ||.x.||) \/ (R_ ||.x.||) by A33, XBOOLE_0:def 3;
a is positive by A33, A4, SURREALI:def 9;
then a <> 0_No by SURREALO:3;
then A36: ( a in (R_ ||.x.||) \ {0_No} & a in dom Y ) by A10, A35, A33, ZFMISC_1:56;
then A37: ( Y . a in Y .: ((R_ ||.x.||) \ {0_No}) & Y .: ((R_ ||.x.||) \ {0_No}) = R_ YY ) by FUNCT_1:def 6;
then reconsider Ya = Y . a as Surreal by SURREAL0:def 16;
a, No_omega^ Ya are_commensurate by A36, A10;
then consider n being positive Nat such that
A38: No_omega^ Ya < a * (uInt . n) ;
A39: uReal . (1 / n) is positive ;
( uInt . n = uDyadic . n & uDyadic . n = uReal . n ) by SURREALN:46, SURREALN:def 5;
then A40: (No_omega^ Ya) * (uReal . (1 / n)) < (a * (uReal . n)) * (uReal . (1 / n)) by A38, A39, SURREALR:70;
(1 / n) * n = 1 by XCMPLX_1:106;
then ( (a * (uReal . n)) * (uReal . (1 / n)) == a * ((uReal . (1 / n)) * (uReal . n)) & a * ((uReal . (1 / n)) * (uReal . n)) == a * 1_No & a * 1_No = a ) by SURREALN:57, SURREALN:48, SURREALR:69, SURREALR:51;
then (a * (uReal . n)) * (uReal . (1 / n)) <= a by SURREALO:4;
then A41: (No_omega^ Ya) * (uReal . (1 / n)) < a by A40, SURREALO:4;
No_omega^ YY <= (No_omega^ Ya) * (uReal . (1 / n)) by A23, Th23, A37;
hence not a <= b by A34, A41, SURREALO:4; :: thesis: verum

end;

A42: x == ||.x.|| by A4, SURREALI:18;
A43: x,||.x.|| are_commensurate by Th8, A4, SURREALI:18;
A44: {||.x.||} << R_ (No_omega^ YY)

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in {||.x.||} or not b in R_ (No_omega^ YY) or not b <= a )
assume A45: ( a in {||.x.||} & b in R_ (No_omega^ YY) ) ; :: thesis: not b <= a
consider xR being Surreal, r being positive Real such that
A46: ( xR in R_ YY & b = (No_omega^ xR) * (uReal . r) ) by A45, Th23;
consider b1 being object such that
A47: ( b1 in dom Y & b1 in (R_ ||.x.||) \ {0_No} & xR = Y . b1 ) by A46, FUNCT_1:def 6;
reconsider b1 = b1 as Surreal by A47, SURREAL0:def 16;
A48: b1, No_omega^ xR are_commensurate by A47, A10;
b1 in R_ x by A47, A4, SURREALI:def 9;
then A49: x <= b1 by A13;
not x, No_omega^ xR are_commensurate by A6, A47, A10, A48;
then x infinitely< No_omega^ xR by Th30, A47, A10, A4, A49;
then x infinitely< b by A46, Th13;
then ||.x.|| < b by Th9, A43, Th15;
hence not b <= a by A45, TARSKI:def 1; :: thesis: verum

end;

A50: L_ (No_omega^ YY) << {||.x.||}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ (No_omega^ YY) or not b in {||.x.||} or not b <= a )
assume A51: ( a in L_ (No_omega^ YY) & b in {||.x.||} ) ; :: thesis: not b <= a

per cases ( a = 0_No or a <> 0_No ) ;

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

then a < ||.x.|| by SURREALI:def 8;
hence not b <= a by A51, TARSKI:def 1; :: thesis: verum

end;

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

then consider xL being Surreal, r being positive Real such that
A52: ( xL in L_ YY & a = (No_omega^ xL) * (uReal . r) ) by A51, Th22;
consider a1 being object such that
A53: ( a1 in dom Y & a1 in (L_ ||.x.||) \ {0_No} & xL = Y . a1 ) by A52, FUNCT_1:def 6;
reconsider a1 = a1 as Surreal by A53, SURREAL0:def 16;
A54: a1, No_omega^ xL are_commensurate by A53, A10;
( a1 in L_ ||.x.|| & a1 <> 0_No ) by A53, ZFMISC_1:56;
then a1 in L_ x by A4, SURREALI:def 9;
then A55: a1 <= x by A13;
not x, No_omega^ xL are_commensurate by A6, A53, A10, A54;
then No_omega^ xL infinitely< x by Th29, A53, A10, A55;
then a < ||.x.|| by A52, A42, SURREALO:4;
hence not b <= a by A51, TARSKI:def 1; :: thesis: verum

end;

end;

end;

No_omega^ YY == ||.x.|| by SURREAL0:43, A24, A44, A50, A32;
then x, No_omega^ YY are_commensurate by Th8, A42, Th5;
hence ex y being Surreal st x, No_omega^ y are_commensurate ; :: thesis: verum

end;

end;

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A2);
then S₁[ born x] ;
hence ex y being Surreal st x, No_omega^ y are_commensurate by A1; :: thesis: verum