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