let a, b be real number ; :: thesis: ( a > 1 & b < 0 implies a to_power b < 1 )
assume A1: ( a > 1 & b < 0 ) ; :: thesis: a to_power b < 1
then a #R b < 1 by PREPOWER:102;
hence a to_power b < 1 by A1, Def2; :: thesis: verum