let
a
be
Real
;
:: thesis:
for
p
being
Rational
st
a
>
0
holds
a
#Q
p
>
0
let
p
be
Rational
;
:: thesis:
(
a
>
0
implies
a
#Q
p
>
0
)
assume
a
>
0
;
:: thesis:
a
#Q
p
>
0
then
A1
:
a
#Z
(
numerator
p
)
>
0
by
Th39
;
denominator
p
>=
1
by
RAT_1:11
;
hence
a
#Q
p
>
0
by
A1
,
Def2
;
:: thesis:
verum