let a, b be Real; :: thesis: ( a > 1 & b < 0 implies a to_power b < 1 )
assume that
A1: a > 1 and
A2: b < 0 ; :: thesis: a to_power b < 1
a #R b < 1 by A1, A2, PREPOWER:88;
hence a to_power b < 1 by A1, Def2; :: thesis: verum