let a, b, c be real number ; :: thesis: ( a > 0 & a < b & c > 0 implies a to_power c < b to_power c )
assume A1: ( a > 0 & a < b & c > 0 ) ; :: thesis: a to_power c < b to_power c
then A2: a to_power c > 0 by Th39;
A3: a to_power c <> 0 by A1, Th39;
a / a < b / a by A1, XREAL_1:76;
then 1 < b / a by A1, XCMPLX_1:60;
then (b / a) to_power c > 1 by A1, Th40;
then (b to_power c) / (a to_power c) > 1 by A1, Th36;
then ((b to_power c) / (a to_power c)) * (a to_power c) > 1 * (a to_power c) by A2, XREAL_1:70;
hence a to_power c < b to_power c by A3, XCMPLX_1:88; :: thesis: verum