let a, b be Real; ( a < b & 0 <= a & b <= 1 implies ex c being Real st
( c in DYADIC & a < c & c < b ) )
assume that
A1:
a < b
and
A2:
0 <= a
and
A3:
b <= 1
; ex c being Real st
( c in DYADIC & a < c & c < b )
set eps = b - a;
consider n being Nat such that
A4:
1 < (2 |^ n) * (b - a)
by A1, Th21, XREAL_1:50;
set aa = (2 |^ n) * a;
set bb = (2 |^ n) * b;
1 < ((2 |^ n) * b) - ((2 |^ n) * a)
by A4;
then consider m being Nat such that
A5:
(2 |^ n) * a < m
and
A6:
m < (2 |^ n) * b
by A2, Th22;
set x = m / (2 |^ n);
take
m / (2 |^ n)
; ( m / (2 |^ n) in DYADIC & a < m / (2 |^ n) & m / (2 |^ n) < b )
A7:
0 < 2 |^ n
by NEWTON:83;
m / (2 |^ n) < b
by A6, NEWTON:83, XREAL_1:83;
then
m / (2 |^ n) < 1
by A3, XXREAL_0:2;
then
m < 2 |^ n
by A7, XREAL_1:181;
then
m / (2 |^ n) in dyadic n
by URYSOHN1:def 1;
hence
( m / (2 |^ n) in DYADIC & a < m / (2 |^ n) & m / (2 |^ n) < b )
by A7, A5, A6, URYSOHN1:def 2, XREAL_1:81, XREAL_1:83; verum