let a, b be Real; :: thesis: ( a < b & 0 <= a & b <= 1 implies ex c being Real st
( c in DYADIC & a < c & c < b ) )
assume A1: ( a < b & 0 <= a & b <= 1 ) ; :: thesis: ex c being Real st
( c in DYADIC & a < c & c < b )
set eps = b - a;
consider n being Element of NAT such that
A2: 1 < (2 |^ n) * (b - a) by Th23, A1, XREAL_1:52;
set aa = (2 |^ n) * a;
set bb = (2 |^ n) * b;
A3: 1 < ((2 |^ n) * b) - ((2 |^ n) * a) by A2;
A4: 0 < 2 |^ n by NEWTON:102;
consider m being Element of NAT such that
A5: ( (2 |^ n) * a < m & m < (2 |^ n) * b ) by A3, Th24, A1;
( a < m / (2 |^ n) & m / (2 |^ n) < b ) by A4, A5, XREAL_1:83, XREAL_1:85;
then m / (2 |^ n) < 1 by A1, XXREAL_0:2;
then A6: ( 0 <= m & m < 2 |^ n ) by A4, XREAL_1:183;
set x = m / (2 |^ n);
A7: m / (2 |^ n) in dyadic n by A6, URYSOHN1:def 3;
take m / (2 |^ n) ; :: thesis: ( m / (2 |^ n) in DYADIC & a < m / (2 |^ n) & m / (2 |^ n) < b )
thus ( m / (2 |^ n) in DYADIC & a < m / (2 |^ n) & m / (2 |^ n) < b ) by A4, A5, A7, URYSOHN1:def 4, XREAL_1:83, XREAL_1:85; :: thesis: verum