let fT be finite Tree; :: thesis: for t being Element of fT st t <> {} holds
height (fT | t) < height fT
let t be Element of fT; :: thesis: ( t <> {} implies height (fT | t) < height fT )
assume t <> {} ; :: thesis: height (fT | t) < height fT
then len t <> 0 ;
then 0 < len t ;
then A1: 0 + 1 <= len t by NAT_1:13;
consider p being FinSequence of NAT such that
A2: ( p in fT | t & len p = height (fT | t) ) by Def15;
t ^ p in fT by A2, Def9;
then ( len (t ^ p) <= height fT & len (t ^ p) = (len t) + (len p) & (len p) + 1 <= (len t) + (len p) ) by A1, Def15, FINSEQ_1:35, XREAL_1:9;
then (height (fT | t)) + 1 <= height fT by A2, XXREAL_0:2;
hence height (fT | t) < height fT by NAT_1:13; :: thesis: verum