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