let a, b be Real; :: thesis: ( a < b implies ex p1, p2 being Rational st
( a < p1 & p1 < p2 & p2 < b ) )
assume a < b ; :: thesis: ex p1, p2 being Rational st
( a < p1 & p1 < p2 & p2 < b )
then consider p1 being Rational such that
A1: a < p1 and
A2: p1 < b by RAT_1:7;
ex p2 being Rational st
( p1 < p2 & p2 < b ) by A2, RAT_1:7;
hence ex p1, p2 being Rational st
( a < p1 & p1 < p2 & p2 < b ) by A1; :: thesis: verum