scheme :: NAT_2:sch 2
Indfrom2{ P₁[ set ] } :

for k being non trivial Nat holds P₁[k]

provided

A1: P₁[2] and
A2: for k being non trivial Nat st P₁[k] holds
P₁[k + 1]