ex k being Nat st
( P₁[k] & ( for n being Nat st P₁[n] holds
k <= n ) )

A1: ex k being Nat st P₁[k]