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