defpred S1[ Nat] means 2 * ($1 - 2) >= $1 - 1;
A1: for n being Nat st n >= 3 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 3 & S1[n] implies S1[n + 1] )
assume that
n >= 3 and
A2: 2 * (n - 2) >= n - 1 ; :: thesis: S1[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: S1[3] ;
 for n being Nat st n >= 3 holds
S1[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