let a, b be real number ; :: thesis: ( a < b implies ex p being Rational st
( a < p & p < b ) )
assume A1: a < b ; :: thesis: ex p being Rational st
( a < p & p < b )
set d = b - a;
set m = [\((b - a) " )/] + 1;
set l = [\(([\((b - a) " )/] + 1) * a)/] + 1;
A2: a - a < b - a by A1, XREAL_1:11;
A3: (b - a) " <= [\((b - a) " )/] + 1 by INT_1:52;
then A4: 0 < [\((b - a) " )/] + 1 by A2;
A5: 0 <> [\((b - a) " )/] + 1 by A2, A3;
reconsider p = ([\(([\((b - a) " )/] + 1) * a)/] + 1) / ([\((b - a) " )/] + 1) as Rational ;
take p ; :: thesis: ( a < p & p < b )
A6: 0 < ([\((b - a) " )/] + 1) " by A4;
thus a < p :: thesis: p < b

proof

(([\((b - a) " )/] + 1) * a) - 1 < [\(([\((b - a) " )/] + 1) * a)/] by INT_1:def 4;
then ([\((b - a) " )/] + 1) * a < [\(([\((b - a) " )/] + 1) * a)/] + 1 by XREAL_1:21;
then (([\((b - a) " )/] + 1) " ) * (([\((b - a) " )/] + 1) * a) < (([\((b - a) " )/] + 1) " ) * ([\(([\((b - a) " )/] + 1) * a)/] + 1) by A6, XREAL_1:70;
then ((([\((b - a) " )/] + 1) " ) * ([\((b - a) " )/] + 1)) * a < (([\((b - a) " )/] + 1) " ) * ([\(([\((b - a) " )/] + 1) * a)/] + 1) ;
then 1 * a < (([\((b - a) " )/] + 1) " ) * ([\(([\((b - a) " )/] + 1) * a)/] + 1) by A5, XCMPLX_0:def 7;
hence a < p ; :: thesis: verum

end;

A7: [\(([\((b - a) " )/] + 1) * a)/] <= ([\((b - a) " )/] + 1) * a by INT_1:def 4;
thus p < b :: thesis: verum

proof

((b - a) " ) - 1 < [\((b - a) " )/] by INT_1:def 4;
then (b - a) " < [\((b - a) " )/] + 1 by XREAL_1:21;
then ((b - a) " ) * (b - a) < ([\((b - a) " )/] + 1) * (b - a) by A2, XREAL_1:70;
then 1 < ([\((b - a) " )/] + 1) * (b - a) by A2, XCMPLX_0:def 7;
then [\(([\((b - a) " )/] + 1) * a)/] + 1 < (([\((b - a) " )/] + 1) * a) + (([\((b - a) " )/] + 1) * (b - a)) by A7, XREAL_1:10;
then (([\((b - a) " )/] + 1) " ) * ([\(([\((b - a) " )/] + 1) * a)/] + 1) < (([\((b - a) " )/] + 1) " ) * (([\((b - a) " )/] + 1) * b) by A6, XREAL_1:70;
then (([\((b - a) " )/] + 1) " ) * ([\(([\((b - a) " )/] + 1) * a)/] + 1) < ((([\((b - a) " )/] + 1) " ) * ([\((b - a) " )/] + 1)) * b ;
then (([\((b - a) " )/] + 1) " ) * ([\(([\((b - a) " )/] + 1) * a)/] + 1) < 1 * b by A5, XCMPLX_0:def 7;
hence p < b ; :: thesis: verum

end;