let a, b be real number ; :: thesis: ( a > 0 implies a to_power b > 0 )
assume A1: a > 0 ; :: thesis: a to_power b > 0
A2: a #R b > 0 by A1, PREPOWER:95;
thus a to_power b > 0 by A1, A2, Def2; :: thesis: verum