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

proof

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume that
A3: k >= 1 and
A4: k ^2 <= 2 * (((k ^2 ) - k) + 1) ; :: thesis: S₁[k + 1]
A5: (k ^2 ) + ((2 * k) + 1) <= (2 * (((k ^2 ) - k) + 1)) + ((2 * k) + 1) by A4, XREAL_1:8;
2 * k >= 2 * 1 by A3, XREAL_1:66;
then A6: (2 * k) + 2 >= 2 + 2 by XREAL_1:8;
A7: (2 * (k ^2 )) + 3 <= (2 * (k ^2 )) + 4 by XREAL_1:8;
(2 * (k ^2 )) + 4 <= (2 * (k ^2 )) + ((2 * k) + 2) by A6, XREAL_1:8;
then (2 * (((k ^2 ) - k) + 1)) + ((2 * k) + 1) <= (2 * (k ^2 )) + ((2 * k) + 2) by A7, XXREAL_0:2;
hence S₁[k + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

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