let k be Nat; :: thesis: k / (k + 1) < 1
defpred S₁[ Nat] means $1 / ($1 + 1) < 1;
A1: S₁[ 0 ] ;
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume m / (m + 1) < 1 ; :: thesis: S₁[m + 1]
m + 1 < (m + 1) + 1 by XREAL_1:31;
hence S₁[m + 1] by XREAL_1:191; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
hence k / (k + 1) < 1 ; :: thesis: verum