theorem :: TREES_3:80

for T being finite Tree holds height (^ T) = (height T) + 1