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 S₁[ Nat] means (((a + $1) + 1) |^ 2) + ((((a + $1) + 1) + x) |^ 2) > ((((a + $1) + 1) + x) + 1) |^ 2;
A2: S₁[ 0 ] by A1, Th46;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
(a + k) + 1 >= 0 + 1 by XREAL_1:6;
hence S₁[k + 1] by A4, Th46; :: thesis: verum

end;

for j being Nat holds S₁[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