theorem Th77: :: TREES_3:77

for n being Nat
for w being FinTree-yielding FinSequence st ( for t being finite Tree st t in rng w holds
height t <= n ) holds
height (tree w) <= n + 1