let eps be Real; :: thesis: ( 0 < eps implies for d being Real st 0 < d 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 0 < eps ; :: thesis: for d being Real st 0 < d 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 )
then consider eps1 being Real such that
A1: 0 < eps1 and
A2: eps1 < eps by XREAL_1:5;
reconsider eps1 = eps1 as Real ;
let d be Real; :: thesis: ( 0 < d 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 A3: 0 < 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 )

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

suppose 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 )

then A4: 0 < d - eps1 by XREAL_1:50;
d - eps1 < d - 0 by A1, XREAL_1:15;
then ex c being Real st
( c in DOM & d - eps1 < c & c < d ) by Th25;
then consider r1 being Real such that
A5: d - eps1 < r1 and
A6: r1 < d and
A7: r1 in DOM ;
( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by A7, URYSOHN1:def 3, XBOOLE_0:def 3;
then A8: ( r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;
eps - eps < eps - eps1 by A2, XREAL_1:15;
then d + 0 < d + (eps - eps1) by XREAL_1:8;
then ex c being Real st
( c in DOM & d < c & c < d + (eps - eps1) ) by Th25;
then consider r2 being Real such that
A9: d < r2 and
A10: r2 < d + (eps - eps1) and
A11: r2 in DOM ;
( r2 in (halfline 0) \/ DYADIC or r2 in right_open_halfline 1 ) by A11, URYSOHN1:def 3, XBOOLE_0:def 3;
then A12: ( r2 in halfline 0 or r2 in DYADIC or r2 in right_open_halfline 1 ) by XBOOLE_0:def 3;
A13: r1 < r2 by A6, A9, XXREAL_0:2;
then A14: d - eps1 < r2 by A5, XXREAL_0:2;
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 )
A15: (d + (eps - eps1)) - (d - eps1) = eps ;
r1 < d + (eps - eps1) by A10, A13, XXREAL_0:2;
then A16: |.(r2 - r1).| < eps by A5, A10, A14, A15, Th30;
0 <= r2 - r1 by A13, XREAL_1:48;
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, A9, A4, A8, A12, A16, ABSVALUE:def 1, XBOOLE_0:def 3, XXREAL_1:233; :: thesis: verum

end;

suppose A17: 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
A18: r1 in DOM and
A19: 0 < r1 and
A20: r1 < d by A3, Th25;
A21: ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by A18, URYSOHN1:def 3, XBOOLE_0:def 3;
0 + d < r1 + eps1 by A17, A19, XREAL_1:8;
then ex c being Real st
( c in DOM & d < c & c < r1 + eps1 ) by Th25;
then consider r2 being Real such that
A22: d < r2 and
A23: r2 < r1 + eps1 and
A24: 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 )
A25: ( r2 in (halfline 0) \/ DYADIC or r2 in right_open_halfline 1 ) by A24, URYSOHN1:def 3, XBOOLE_0:def 3;
not r1 in halfline 0 by A19, XXREAL_1:233;
then A26: ( r1 in DYADIC or r1 in right_open_halfline 1 ) by A21, XBOOLE_0:def 3;
not r2 in halfline 0 by A3, A22, XXREAL_1:233;
then A27: ( r2 in DYADIC or r2 in right_open_halfline 1 ) by A25, XBOOLE_0:def 3;
r2 - r1 < (r1 + eps1) - r1 by A23, XREAL_1:9;
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 A2, A19, A20, A22, A26, A27, XBOOLE_0:def 3, XXREAL_0:2; :: thesis: verum

end;

end;