let a be real number ; :: 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 A1: a > 0 ; :: thesis: a #Q p > 0
A2: denominator p >= 1 by RAT_1:29;
a #Z (numerator p) > 0 by A1, Th49;
hence a #Q p > 0 by A2, Def3; :: thesis: verum