for a being Real
for p, q being Rational st a >= 1 & p >= q holds
a #Q p >= a #Q q