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

proof

let k be Nat; :: thesis: ( k >= 2 & S₁[k] implies S₁[k + 1] )
assume that
A2: k >= 2 and
A3: k ^2 > k + 1 ; :: thesis: S₁[k + 1]
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: verum

end;

A5: S₁[2] ;
for n being Nat st n >= 2 holds
S₁[n] from NAT_1:sch 8(A5, A1);
hence for n being Nat st n >= 2 holds
n ^2 > n + 1 ; :: thesis: verum