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 Def15;
A3: t ^ p in fT by A1, Def9;
A4: len (t ^ p) <= height fT by A3, Def15;
A5: ( len (t ^ p) = (len t) + (len p) & len p <= (len p) + (len t) ) by FINSEQ_1:35, NAT_1:11;
thus height (fT | t) <= height fT by A2, A4, A5, XXREAL_0:2; :: thesis: verum