for w being FinTree-yielding FinSequence
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