defpred S₁[ Nat] means 2 * ($1 - 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
n >= 3 and
A2: 2 * (n - 2) >= n - 1 ; :: thesis: S₁[n + 1]
(2 * (n - 2)) + 2 >= (n + (- 1)) + 1 by A2, XREAL_1:7;
hence 2 * ((n + 1) - 2) >= (n + 1) - 1 ; :: thesis: verum

end;

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