A1: ex n being Element of NAT st
( n > 1 & P₁[n] ) and
A2: for k being Element of NAT st k >= 1 & P₁[k + 1] holds
P₁[k]