theorem Th46: :: NEWTON01:47

for a, x being Nat st a >= 1 & ((a + 1) |^ 2) + (((a + 1) + x) |^ 2) <= (((a + 1) + x) + 1) |^ 2 holds
(a |^ 2) + ((a + x) |^ 2) < ((a + x) + 1) |^ 2