let k be Nat; :: thesis: P₁[k]
defpred S₁[ Nat] means for n being Nat st n < $1 holds
P₁[n];
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: for n being Nat st n < k holds
P₁[n] ; :: thesis: S₁[k + 1]
let n be Nat; :: thesis: ( n < k + 1 implies P₁[n] )
assume n < k + 1 ; :: thesis: P₁[n]
then n <= k by Th8;
then ( n < k or ( n = k & n <= k ) ) by XXREAL_0:1;
hence P₁[n] by A1, A3; :: thesis: verum

end;

A4: S₁[ 0 ] by Th2;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
then for n being Nat st n < k holds
P₁[n] ;
hence P₁[k] by A1; :: thesis: verum