let w be FinTree-yielding FinSequence; :: thesis: for t being finite Tree st t in rng w & ( for t9 being finite Tree st t9 in rng w holds
height t9 <= height t ) holds
height (tree w) = (height t) + 1
let t be finite Tree; :: thesis: ( t in rng w & ( for t9 being finite Tree st t9 in rng w holds
height t9 <= height t ) implies height (tree w) = (height t) + 1 )
assume that
A1: t in rng w and
A2: for t9 being finite Tree st t9 in rng w holds
height t9 <= height t ; :: thesis: height (tree w) = (height t) + 1
A3: height (tree w) > height t by A1, Th78;
A4: height (tree w) <= (height t) + 1 by A2, Th77;
height (tree w) >= (height t) + 1 by A3, NAT_1:13;
hence height (tree w) = (height t) + 1 by A4, XXREAL_0:1; :: thesis: verum