let a, b, c, x be Nat; :: thesis: ( x > 0 & b < c & a + (b |^ 2) = c |^ 2 implies a + ((b + x) |^ 2) < (c + x) |^ 2 )
assume A1: ( x > 0 & b < c & a + (b |^ 2) = c |^ 2 ) ; :: thesis: a + ((b + x) |^ 2) < (c + x) |^ 2
then A1a: b - c < c - c by XREAL_1:9;
(a + ((b + x) |^ 2)) - ((c + x) |^ 2) = (2 * x) * (b - c) by A1, Lm61;
then ((a + ((b + x) |^ 2)) - ((c + x) |^ 2)) + ((c + x) |^ 2) < 0 + ((c + x) |^ 2) by A1, A1a, XREAL_1:6;
hence a + ((b + x) |^ 2) < (c + x) |^ 2 ; :: thesis: verum