theorem Th45: :: TREES_9:45

for n being Nat
for T being Tree holds T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }