P₁[ 0 ]

A1: ex k being Nat st P₁[k] and
A2: for k being Nat st k <> 0 & P₁[k] holds
ex n being Nat st
( n < k & P₁[n] )