let n be Nat; :: thesis: for r being Real st n is odd & r < 0 holds
r to_power n < 0
let r be Real; :: thesis: ( n is odd & r < 0 implies r to_power n < 0 )
assume A1: n is odd ; :: thesis: ( not r < 0 or r to_power n < 0 )
assume A2: r < 0 ; :: thesis: r to_power n < 0
A3: r to_power n = (- (- r)) to_power n
.= - ((- r) to_power n) by Th4, A1, A2 ;
(- r) to_power n > 0 by A2, POWER:34;
hence r to_power n < 0 by A3; :: thesis: verum