let fT be finite Tree; :: thesis: for t being Element of fT holds height (fT | t) <= height fT
let t be Element of fT; :: thesis: height (fT | t) <= height fT
consider p being FinSequence of NAT such that
A1: ( p in fT | t & len p = height (fT | t) ) by Def15;
t ^ p in fT by A1, Def9;
then ( len (t ^ p) <= height fT & len (t ^ p) = (len t) + (len p) & (len p) + (len t) = (len t) + (len p) & len p <= (len p) + (len t) ) by Def15, FINSEQ_1:35, NAT_1:11;
hence height (fT | t) <= height fT by A1, XXREAL_0:2; :: thesis: verum