let eps be Real; :: thesis: ( 0 < eps implies for d being Real st 0 < d & d <= 1 holds
ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) )
assume A1: 0 < eps ; :: thesis: for d being Real st 0 < d & d <= 1 holds
ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
let d be Real; :: thesis: ( 0 < d & d <= 1 implies ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) )
assume A2: ( 0 < d & d <= 1 ) ; :: thesis: ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
consider eps1 being real number such that
A3: ( 0 < eps1 & eps1 < eps ) by A1, XREAL_1:7;
reconsider eps1 = eps1 as Real by XREAL_0:def 1;

per cases ( eps1 < d or d <= eps1 ) ;

suppose A4: eps1 < d ; :: thesis: ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )

d - eps1 < d - 0 by A3, XREAL_1:17;
then ex c being Real st
( c in DOM & d - eps1 < c & c < d ) by Th29;
then consider r1 being Real such that
A5: ( d - eps1 < r1 & r1 < d & r1 in DOM ) ;
eps - eps < eps - eps1 by A3, XREAL_1:17;
then d + 0 < d + (eps - eps1) by XREAL_1:10;
then ex c being Real st
( c in DOM & d < c & c < d + (eps - eps1) ) by Th29;
then consider r2 being Real such that
A6: ( d < r2 & r2 < d + (eps - eps1) & r2 in DOM ) ;
take r1 ; :: thesis: ex r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
take r2 ; :: thesis: ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
A7: 0 < d - eps1 by A4, XREAL_1:52;
( ( r1 in (halfline 0 ) \/ DYADIC or r1 in right_open_halfline 1 ) & ( r2 in (halfline 0 ) \/ DYADIC or r2 in right_open_halfline 1 ) ) by A5, A6, URYSOHN1:def 5, XBOOLE_0:def 3;
then A8: ( ( r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 ) & ( r2 in halfline 0 or r2 in DYADIC or r2 in right_open_halfline 1 ) ) by XBOOLE_0:def 3;
A9: r1 < r2 by A5, A6, XXREAL_0:2;
then A10: r1 < d + (eps - eps1) by A6, XXREAL_0:2;
A11: d - eps1 < r2 by A5, A9, XXREAL_0:2;
(d + (eps - eps1)) - (d - eps1) = eps ;
then A12: abs (r2 - r1) < eps by A5, A6, A10, A11, Th34;
0 <= r2 - r1 by A9, XREAL_1:50;
hence ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) by A5, A6, A7, A8, A12, ABSVALUE:def 1, XBOOLE_0:def 3, XXREAL_1:233; :: thesis: verum

end;

suppose A13: d <= eps1 ; :: thesis: ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )

consider r1 being Real such that
A14: ( r1 in DOM & 0 < r1 & r1 < d ) by A2, Th29;
0 + d < r1 + eps1 by A13, A14, XREAL_1:10;
then ex c being Real st
( c in DOM & d < c & c < r1 + eps1 ) by Th29;
then consider r2 being Real such that
A15: ( d < r2 & r2 < r1 + eps1 & r2 in DOM ) ;
take r1 ; :: thesis: ex r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
take r2 ; :: thesis: ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
A16: not r1 in halfline 0 by A14, XXREAL_1:233;
A17: not r2 in halfline 0 by A2, A15, XXREAL_1:233;
( ( r1 in (halfline 0 ) \/ DYADIC or r1 in right_open_halfline 1 ) & ( r2 in (halfline 0 ) \/ DYADIC or r2 in right_open_halfline 1 ) ) by A14, A15, URYSOHN1:def 5, XBOOLE_0:def 3;
then A18: ( ( r1 in DYADIC or r1 in right_open_halfline 1 ) & ( r2 in DYADIC or r2 in right_open_halfline 1 ) ) by A16, A17, XBOOLE_0:def 3;
r2 - r1 < (r1 + eps1) - r1 by A15, XREAL_1:11;
hence ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) by A3, A14, A15, A18, XBOOLE_0:def 3, XXREAL_0:2; :: thesis: verum

end;

end;