theorem Th3: :: FIB_NUM3:3

for a being Real holds a to_power 2 = (- a) to_power 2