assume A2: for k being Nat holds
( not P₁[k] or ex n being Nat st
( P₁[n] & not k <= n ) ) ; :: thesis: contradiction
defpred S₁[ Nat] means P₁[$1];
A3: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
A4: ( ( for n being Nat holds
( not P₁[n] or k <= n ) ) implies not P₁[k] ) by A2;
assume for n being Nat st n < k holds
not P₁[n] ; :: thesis: S₁[k]
hence S₁[k] by A4; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A3);
hence contradiction by A1; :: thesis: verum