consider k being Nat such that
A3: ( P₁[k] & ( for n being Nat st P₁[n] holds
k <= n ) ) from NAT_1:sch 5(A1);

now :: thesis: not k <> 0

assume k <> 0 ; :: thesis: contradiction
then ex n being Nat st
( n < k & P₁[n] ) by A2, A3;
hence contradiction by A3; :: thesis: verum

end;

hence P₁[ 0 ] by A3; :: thesis: verum