defpred S₁[ Nat] means $1 ^2 > $1 + 1;
A1: for k being Nat st k >= 2 & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume that
A2: k >= 2 and
A3: k ^2 > k + 1 ; :: thesis:
2 * k > 2 * 0 by A2, XREAL_1:68;
then (2 * k) + 1 > 0 + 1 by XREAL_1:6;
then A4: (k + 1) + ((2 * k) + 1) > (k + 1) + 1 by XREAL_1:6;
(k ^2) + ((2 * k) + 1) > (k + 1) + ((2 * k) + 1) by A3, XREAL_1:6;
hence (k + 1) ^2 > (k + 1) + 1 by A4, XXREAL_0:2; :: thesis:

end;