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 }