let a be real number ; :: thesis: for p, q being Rational st a >= 1 & p >= q holds
a #Q p >= a #Q q
let p, q be Rational; :: thesis: ( a >= 1 & p >= q implies a #Q p >= a #Q q )
assume A1: ( a >= 1 & p >= q ) ; :: thesis: a #Q p >= a #Q q

per cases ( p = q or p > q ) by A1, XXREAL_0:1;

suppose p = q ; :: thesis: a #Q p >= a #Q q

hence a #Q p >= a #Q q ; :: thesis: verum

end;

suppose p > q ; :: thesis: a #Q p >= a #Q q

then A2: p - q >= 0 by XREAL_1:52;
A3: ( a #Q q <> 0 & a #Q q >= 0 ) by A1, Th63;
(a #Q p) / (a #Q q) = a #Q (p - q) by A1, Th66;
then ((a #Q p) / (a #Q q)) * (a #Q q) >= 1 * (a #Q q) by A1, A2, A3, Th71, XREAL_1:66;
hence a #Q p >= a #Q q by A3, XCMPLX_1:88; :: thesis: verum

end;

end;