theorem Th13: :: BKMODEL1:15

for a, b being Real st a <> 0 & - 1 < a & a < 1 & b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a) holds
(((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0