consider k being Nat such that
A3: ( P1[k] & ( for n being Nat st P1[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 & P1[n] ) by A2, A3;
hence contradiction by A3; :: thesis: verum
end;
hence P1[ 0 ] by A3; :: thesis: verum