defpred S₁[ Nat] means for n being Nat st P₁[n] holds
n <= $1;
A3: ex k being Nat st S₁[k] by A1;
consider k being Nat such that
A4: S₁[k] and
A5: for m being Nat st S₁[m] holds
k <= m from NAT_1:sch 5(A3);
take k ; :: thesis: ( P₁[k] & ( for n being Nat st P₁[n] holds
n <= k ) )
thus P₁[k] :: thesis: for n being Nat st P₁[n] holds
n <= k

proof

consider n being Nat such that
A6: P₁[n] by A2;
A7: n <= k by A4, A6;
assume A8: P₁[k] ; :: thesis: contradiction
then n <> k by A6;
then k <> 0 by A7, Th2;
then consider m being Nat such that
A9: k = m + 1 by Th6;
A10: for n being Nat st P₁[n] holds
n <= m by A4, A8, A9, Th8;
((- m) + m) + 1 = (- m) + (m + 1) ;
hence contradiction by A5, A9, A10, XREAL_1:6; :: thesis: verum

end;

thus for n being Nat st P₁[n] holds
n <= k by A4; :: thesis: verum