theorem :: TREES_1:46

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