theorem :: TREES_3:81

for T1, T2 being finite Tree holds height (tree (T1,T2)) = (max ((height T1),(height T2))) + 1