let a, b be real number ; :: 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
A3: a #R b > 1 by A1, A2, PREPOWER:100;
thus a to_power b > 1 by A1, A3, Def2; :: thesis: verum