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

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

end;

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