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
reconsider q = 0 as Rational ;
A2: 1 / a > 1 by A1, Lm4, XREAL_1:90;
then (1 / a) #Q p > (1 / a) #Q q by A1, Th75;
then (1 / a) #Q p > 1 by A2, Th58;
then 1 / (a #Q p) > 1 by A1, Th68;
hence a #Q p < 1 by XREAL_1:187; :: thesis: verum