scheme :: TREES_1:sch 1
TreeInd{ P₁[ Tree] } :

for fT being finite Tree holds P₁[fT]

provided

A1: for fT being finite Tree st ( for n being Element of NAT st <*n*> in fT holds
P₁[fT | <*n*>] ) holds
P₁[fT]