defpred S1[ set ] means for fT being finite Tree st height fT = $1 holds
P1[fT];
A2: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A3: for k being Nat st k < n holds
for fT being finite Tree st height fT = k holds
P1[fT] ; :: thesis: S1[n]
let fT be finite Tree; :: thesis: ( height fT = n implies P1[fT] )
assume A4: height fT = n ; :: thesis: P1[fT]
now :: thesis: for k being Element of NAT st <*k*> in fT holds
P1[fT | <*k*>]
let k be Element of NAT ; :: thesis: ( <*k*> in fT implies P1[fT | <*k*>] )
assume <*k*> in fT ; :: thesis: P1[fT | <*k*>]
then reconsider k9 = <*k*> as Element of fT ;
height (fT | k9) < height fT by Th47;
hence P1[fT | <*k*>] by A3, A4; :: thesis: verum
end;
hence P1[fT] by A1; :: thesis: verum
end;
A5: for n being Nat holds S1[n] from NAT_1:sch 4(A2);
 let fT be finite Tree; :: thesis: P1[fT]
height fT = height fT ;
hence P1[fT] by A5; :: thesis: verum