theorem Th54: :: TREES_3:54

for i being Nat holds elementary_tree i = tree (i |-> (elementary_tree 0))