for k being Nat holds P₁[k]

A1: P₁[ 0 ] and
A2: P₁[1] and
A3: for k being Nat st P₁[k] & P₁[k + 1] holds
P₁[k + 2]