scheme :: TREES_1:sch 1
TreeInd{ P1[ Tree] } :
for fT being finite Tree holds P1[fT]
provided
A1: for fT being finite Tree st ( for n being Element of NAT st <*n*> in fT holds
P1[fT | <*n*>] ) holds
P1[fT]