let n be natural number ; :: thesis: for r being real number st not n is even & r < 0 holds
r to_power n < 0
let r be real number ; :: thesis: ( not n is even & r < 0 implies r to_power n < 0 )
assume A1: not n is even ; :: 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