theorem :: PREPOWER:66
for a being Real
for p being Rational st a > 0 & a <= 1 & p <= 0 holds
a #Q p >= 1