let a be Real; :: thesis: for p being Rational st a >= 1 & p <= 0 holds
a #Q p <= 1
let p be Rational; :: thesis: ( a >= 1 & p <= 0 implies a #Q p <= 1 )
assume that
A1: a >= 1 and
A2: p <= 0 ; :: thesis: a #Q p <= 1
a #Q (- p) >= 1 by A1, A2, Th60;
then 1 / (a #Q p) >= 1 by A1, Th54;
hence a #Q p <= 1 by XREAL_1:191; :: thesis: verum