theorem :: TREES_1:44

for n being Nat holds height (elementary_tree (n + 1)) = 1