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 A0: not n is even ; :: thesis: ( not r < 0 or r to_power n < 0 )
assume A1: r < 0 ; :: thesis: r to_power n < 0
d6: r to_power n = (- (- r)) to_power n
.= - ((- r) to_power n) by pomoc2, A0, A1 ;
(- r) to_power n > 0 by A1, POWER:39;
hence r to_power n < 0 by d6; :: thesis: verum