let n be Nat; :: thesis: for r being Real holds
( uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) < sReal . r & sReal . r < uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) )
let r be Real; :: thesis: ( uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) < sReal . r & sReal . r < uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) )
set R = sReal . r;
( L_ (sReal . r) << {(sReal . r)} & {(sReal . r)} << R_ (sReal . r) & sReal . r in {(sReal . r)} ) by SURREALO:11, TARSKI:def 1;
hence ( uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) < sReal . r & sReal . r < uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) ) by Th42, Th43; :: thesis: verum