theorem :: RAT_1:7

for a, b being Real st a < b holds
ex p being Rational st
( a < p & p < b )