let
p
,
r
be
Real
;
:: thesis:
(
r
>
p
implies ex
q
being
Rational
st
q
in
[.
p
,
r
.[
)
assume
A1
:
r
>
p
;
:: thesis:
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
;
:: thesis:
verum