defpred S₁[ set ] means for fT being finite Tree st height fT = $1 holds
P₁[fT];
A2: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A3: for k being Nat st k < n holds
for fT being finite Tree st height fT = k holds
P₁[fT] ; :: thesis: S₁[n]
let fT be finite Tree; :: thesis: ( height fT = n implies P₁[fT] )
assume A4: height fT = n ; :: thesis: P₁[fT]

now :: thesis: for k being Element of NAT st <*k*> in fT holds
P₁[fT | <*k*>]

let k be Element of NAT ; :: thesis: ( <*k*> in fT implies P₁[fT | <*k*>] )
assume <*k*> in fT ; :: thesis: P₁[fT | <*k*>]
then reconsider k9 = <*k*> as Element of fT ;
height (fT | k9) < height fT by Th47;
hence P₁[fT | <*k*>] by A3, A4; :: thesis: verum

end;

hence P₁[fT] by A1; :: thesis: verum

end;

A5: for n being Nat holds S₁[n] from NAT_1:sch 4(A2);
let fT be finite Tree; :: thesis: P₁[fT]
height fT = height fT ;
hence P₁[fT] by A5; :: thesis: verum