set x = frac number_e ;
let a, b be real number ; ( a < b implies ex p being real irrational number st
( a < p & p < b ) )
A1:
frac number_e < 1
by INT_1:69;
assume
a < b
; ex p being real irrational number st
( a < p & p < b )
then consider p1, p2 being rational number such that
A2:
a < p1
and
A3:
p1 < p2
and
A4:
p2 < b
by Th47;
set y = ((1 - (frac number_e )) * p1) + ((frac number_e ) * p2);
A5:
0 < frac number_e
by INT_1:69;
then
((1 - (frac number_e )) * p1) + ((frac number_e ) * p2) < p2
by A3, A1, XREAL_1:180;
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:179;
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 real irrational number st
( a < p & p < b )
by A8, A6, A7; verum