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 and
A2: len p = height (fT | t) by Def12;
t ^ p in fT by A1, Def6;
then A3: len (t ^ p) <= height fT by Def12;
( len (t ^ p) = (len t) + (len p) & len p <= (len p) + (len t) ) by FINSEQ_1:22, NAT_1:11;
hence height (fT | t) <= height fT by A2, A3, XXREAL_0:2; :: thesis: verum