let a be real number ; :: thesis: for p being Rational st a > 0 & a <= 1 & p <= 0 holds
a #Q p >= 1
let p be Rational; :: thesis: ( a > 0 & a <= 1 & p <= 0 implies a #Q p >= 1 )
assume A1: ( a > 0 & a <= 1 & p <= 0 ) ; :: thesis: a #Q p >= 1
then 1 / a >= 1 by Lm4, XREAL_1:87;
then (1 / a) #Q p <= 1 by A1, Th72;
then A2: 1 / (a #Q p) <= 1 by A1, Th68;
a #Q p > 0 by A1, Th63;
hence a #Q p >= 1 by A2, XREAL_1:189; :: thesis: verum