let p, r be Real; ( r > p implies ex q being Rational st q in [.p,r.[ )
assume A1:
r > p
; ex q being Rational st q in [.p,r.[
consider q being Rational such that
A2:
( p < q & q < r )
by A1, RAT_1:7;
thus
ex q being Rational st q in [.p,r.[
by A2, XXREAL_1:3; verum