let a, b be Real; :: thesis: ( a < b implies ex c being Real st
( c in DOM & a < c & c < b ) )
assume A1: a < b ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

per cases ( ( a < 0 & b <= 1 ) or ( a < 0 & 1 < b ) or ( 0 <= a & b <= 1 ) or ( 0 <= a & 1 < b ) ) ;

suppose A2: ( a < 0 & b <= 1 ) ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

now :: thesis: ( ( b <= 0 & ex c being Real st
( c in DOM & a < c & c < b ) ) or ( 0 < b & ex c being Real st
( c in DOM & a < c & c < b ) ) )

per cases ( b <= 0 or 0 < b ) ;

case A3: b <= 0 ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

consider c being Real such that
A4: a < c and
A5: c < b by A1, XREAL_1:5;
reconsider c = c as Real ;
halfline 0 = { g where g is Real : g < 0 } by XXREAL_1:229;
then c in halfline 0 by A3, A5;
then c in (halfline 0) \/ DYADIC by XBOOLE_0:def 3;
then c in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
hence ex c being Real st
( c in DOM & a < c & c < b ) by A4, A5; :: thesis: verum

end;

case A6: 0 < b ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

set a1 = 0 ;
consider c being Real such that
A7: c in DYADIC and
A8: ( 0 < c & c < b ) by A2, A6, Th24;
c in (halfline 0) \/ DYADIC by A7, XBOOLE_0:def 3;
then c in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
hence ex c being Real st
( c in DOM & a < c & c < b ) by A2, A8; :: thesis: verum

end;

end;

end;

hence ex c being Real st
( c in DOM & a < c & c < b ) ; :: thesis: verum

end;

suppose A9: ( a < 0 & 1 < b ) ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

consider a1, b1 being Real such that
A10: ( a1 = 0 & b1 = 1 ) ;
consider c being Real such that
A11: c in DYADIC and
A12: ( a1 < c & c < b1 ) by A10, Th24;
take c ; :: thesis: ( c in DOM & a < c & c < b )
c in (halfline 0) \/ DYADIC by A11, XBOOLE_0:def 3;
hence ( c in DOM & a < c & c < b ) by A9, A10, A12, URYSOHN1:def 3, XBOOLE_0:def 3, XXREAL_0:2; :: thesis: verum

end;

suppose ( 0 <= a & b <= 1 ) ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

then consider c being Real such that
A13: c in DYADIC and
A14: ( a < c & c < b ) by A1, Th24;
take c ; :: thesis: ( c in DOM & a < c & c < b )
c in (halfline 0) \/ DYADIC by A13, XBOOLE_0:def 3;
hence ( c in DOM & a < c & c < b ) by A14, URYSOHN1:def 3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A15: ( 0 <= a & 1 < b ) ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

now :: thesis: ( ( 1 <= a & ex c being Real st
( c in DOM & a < c & c < b ) ) or ( a < 1 & ex c being Real st
( c in DOM & a < c & c < b ) ) )

per cases ( 1 <= a or a < 1 ) ;

case A16: 1 <= a ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

consider c being Real such that
A17: a < c and
A18: c < b by A1, XREAL_1:5;
reconsider c = c as Real ;
( right_open_halfline 1 = { g where g is Real : 1 < g } & 1 < c ) by A16, A17, XXREAL_0:2, XXREAL_1:230;
then c in right_open_halfline 1 ;
then c in DYADIC \/ (right_open_halfline 1) by XBOOLE_0:def 3;
then c in (halfline 0) \/ (DYADIC \/ (right_open_halfline 1)) by XBOOLE_0:def 3;
then c in DOM by URYSOHN1:def 3, XBOOLE_1:4;
hence ex c being Real st
( c in DOM & a < c & c < b ) by A17, A18; :: thesis: verum

end;

case A19: a < 1 ; :: thesis: ex c being Real st
( c in DOM & a < c & c < b )

set b1 = 1;
consider c being Real such that
A20: c in DYADIC and
A21: a < c and
A22: c < 1 by A15, A19, Th24;
c in (halfline 0) \/ DYADIC by A20, XBOOLE_0:def 3;
then A23: c in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
c < b by A15, A22, XXREAL_0:2;
hence ex c being Real st
( c in DOM & a < c & c < b ) by A21, A23; :: thesis: verum

end;

end;

end;

hence ex c being Real st
( c in DOM & a < c & c < b ) ; :: thesis: verum

end;

end;