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 A2: 0 + 1 <= len t by NAT_1:13;
consider p being FinSequence of NAT such that
A3: p in fT | t and
A4: len p = height (fT | t) by Def15;
t ^ p in fT by A3, Def9;
then A6: len (t ^ p) <= height fT by Def15;
( len (t ^ p) = (len t) + (len p) & (len p) + 1 <= (len t) + (len p) ) by A2, FINSEQ_1:35, XREAL_1:9;
then (height (fT | t)) + 1 <= height fT by A4, A6, XXREAL_0:2;
hence height (fT | t) < height fT by NAT_1:13; :: thesis: verum