defpred S₁[ Nat] means $1 ^2 > (2 * $1) + 1;
A1: for n being Nat st n >= 3 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 3 & S₁[n] implies S₁[n + 1] )
assume that
A2: n >= 3 and
A3: n ^2 > (2 * n) + 1 ; :: thesis: S₁[n + 1]
n > 1 by A2, XXREAL_0:2;
then n + n > 1 + 0 by XREAL_1:8;
then A4: (2 * n) + (2 * (n + 1)) > 1 + (2 * (n + 1)) by XREAL_1:6;
(n ^2) + (n + (n + 1)) > ((2 * n) + 1) + (n + (n + 1)) by A3, XREAL_1:6;
hence (n + 1) ^2 > (2 * (n + 1)) + 1 by A4, XXREAL_0:2; :: thesis: verum

end;

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