theorem Th7: :: FIB_NUM4:7
for n being Nat
for r being Real st n is odd & r < 0 holds
r to_power n < 0