let a, x, l be Nat; :: thesis: ( a >= 1 & (a |^ 2) + ((a + x) |^ 2) >= ((a + x) + 1) |^ 2 implies (((a + l) + 1) |^ 2) + ((((a + l) + 1) + x) |^ 2) > ((((a + l) + 1) + x) + 1) |^ 2 )
assume A1: ( a >= 1 & (a |^ 2) + ((a + x) |^ 2) >= ((a + x) + 1) |^ 2 ) ; :: thesis: (((a + l) + 1) |^ 2) + ((((a + l) + 1) + x) |^ 2) > ((((a + l) + 1) + x) + 1) |^ 2
defpred S1[ Nat] means (((a + $1) + 1) |^ 2) + ((((a + $1) + 1) + x) |^ 2) > ((((a + $1) + 1) + x) + 1) |^ 2;
A2: S1[ 0 ] by A1, Th46;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
(a + k) + 1 >= 0 + 1 by XREAL_1:6;
hence S1[k + 1] by A4, Th46; :: thesis: verum
end;
for j being Nat holds S1[j] from NAT_1:sch 2(A2, A3);
 hence (((a + l) + 1) |^ 2) + ((((a + l) + 1) + x) |^ 2) > ((((a + l) + 1) + x) + 1) |^ 2 ; :: thesis: verum