let r be Real; :: thesis: sReal . r in Day omega
set X1 = { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } ;
set X2 = { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } ;
A1: for o being object st o in { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } \/ { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } holds
ex O being Ordinal st
( O in NAT & o in Day O )

proof

let o be object ; :: thesis: ( o in { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } \/ { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } implies ex O being Ordinal st
( O in NAT & o in Day O ) )
assume o in { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } \/ { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } ; :: thesis: ex O being Ordinal st
( O in NAT & o in Day O )
then ( o in { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } or o in { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } ) by XBOOLE_0:def 3;
then consider n being Nat such that
A2: ( o = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) or o = uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) ) ;
reconsider o = o as Surreal by A2;
take born o ; :: thesis: ( born o in NAT & o in Day (born o) )
born o is finite by Th37, A2;
hence ( born o in NAT & o in Day (born o) ) by SURREAL0:def 18, ORDINAL1:def 12; :: thesis: verum

end;

{ (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } << { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum }

proof

let L, R be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not L in { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } or not R in { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } or not R <= L )
assume A3: ( L in { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } & R in { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } ) ; :: thesis: not R <= L
consider n being Nat such that
A4: L = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) by A3;
consider m being Nat such that
A5: R = uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m)) by A3;
( [/((r * (2 |^ n)) - 1)\] / (2 |^ n) < r & r < [\((r * (2 |^ m)) + 1)/] / (2 |^ m) ) by Th41;
then [/((r * (2 |^ n)) - 1)\] / (2 |^ n) < [\((r * (2 |^ m)) + 1)/] / (2 |^ m) by XXREAL_0:2;
hence not R <= L by A4, A5, Th24; :: thesis: verum

end;

then [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n))) where n is Nat : verum } ] in Day omega by A1, SURREAL0:46;
hence sReal . r in Day omega by Def6; :: thesis: verum