theorem Th47: :: NEWTON01:48

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