theorem :: TREES_2:39

for n being Nat holds TrivialInfiniteTree -level n = {(n |-> 0)}