set x = frac number_e;
let a, b be Real; ( a < b implies ex p being irrational Real st
( a < p & p < b ) )
A1:
frac number_e < 1
by INT_1:43;
assume
a < b
; ex p being irrational Real st
( a < p & p < b )
then consider p1, p2 being Rational such that
A2:
a < p1
and
A3:
p1 < p2
and
A4:
p2 < b
by Th25;
set y = ((1 - (frac number_e)) * p1) + ((frac number_e) * p2);
A5:
0 < frac number_e
by INT_1:43;
then
((1 - (frac number_e)) * p1) + ((frac number_e) * p2) < p2
by A3, A1, XREAL_1:178;
then A6:
((1 - (frac number_e)) * p1) + ((frac number_e) * p2) < b
by A4, XXREAL_0:2;
((1 - (frac number_e)) * p1) + ((frac number_e) * p2) > p1
by A3, A5, A1, XREAL_1:177;
then A7:
((1 - (frac number_e)) * p1) + ((frac number_e) * p2) > a
by A2, XXREAL_0:2;
A8:
((1 - (frac number_e)) * p1) + ((frac number_e) * p2) = p1 + ((frac number_e) * (p2 - p1))
;
p2 - p1 <> 0
by A3;
hence
ex p being irrational Real st
( a < p & p < b )
by A8, A6, A7; verum