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