scheme :: FIB_NUM:sch 1
FibInd{ P₁[ set ] } :

for k being Nat holds P₁[k]

provided

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