defpred S₁[ Nat] means $1 ^2 > (2 * $1) + 1;
A1: S₁[3] ;
A2: 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
A3: n >= 3 and
A4: n ^2 > (2 * n) + 1 ; :: thesis: S₁[n + 1]
A5: (n ^2 ) + (n + (n + 1)) > ((2 * n) + 1) + (n + (n + 1)) by A4, XREAL_1:8;
( n > 0 & n > 1 ) by A3, XXREAL_0:2;
then n + n > 1 + 0 by XREAL_1:10;
then (2 * n) + (2 * (n + 1)) > 1 + (2 * (n + 1)) by XREAL_1:8;
hence (n + 1) ^2 > (2 * (n + 1)) + 1 by A5, XXREAL_0:2; :: thesis: verum

end;

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