let a, b be Real; :: thesis: ( a < b implies 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;
set p = ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1);
assume a < b ; :: thesis: ex p being Rational st
( a < p & p < b )
then A1: a - a < b - a by XREAL_1:9;
then A2: 0 < [\((b - a) ")/] + 1 by INT_1:29;
((b - a) ") - 1 < [\((b - a) ")/] by INT_1:def 6;
then (b - a) " < [\((b - a) ")/] + 1 by XREAL_1:19;
then ((b - a) ") * (b - a) < ([\((b - a) ")/] + 1) * (b - a) by A1, XREAL_1:68;
then A3: 1 < ([\((b - a) ")/] + 1) * (b - a) by A1, XCMPLX_0:def 7;
take ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) ; :: thesis: ( a < ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) & ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) < b )
A4: 0 <> [\((b - a) ")/] + 1 by A1, INT_1:29;
(([\((b - a) ")/] + 1) * a) - 1 < [\(([\((b - a) ")/] + 1) * a)/] by INT_1:def 6;
then ([\((b - a) ")/] + 1) * a < [\(([\((b - a) ")/] + 1) * a)/] + 1 by XREAL_1:19;
then (([\((b - a) ")/] + 1) ") * (([\((b - a) ")/] + 1) * a) < (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) by A2, XREAL_1:68;
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 A4, XCMPLX_0:def 7;
hence a < ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) ; :: thesis: ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) < b
[\(([\((b - a) ")/] + 1) * a)/] <= ([\((b - a) ")/] + 1) * a by INT_1:def 6;
then [\(([\((b - a) ")/] + 1) * a)/] + 1 < (([\((b - a) ")/] + 1) * a) + (([\((b - a) ")/] + 1) * (b - a)) by A3, XREAL_1:8;
then (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) < (([\((b - a) ")/] + 1) ") * (([\((b - a) ")/] + 1) * b) by A2, XREAL_1:68;
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 A4, XCMPLX_0:def 7;
hence ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) < b ; :: thesis: verum