theorem :: TREES_2:16

for W being Tree
for L being Level of W ex n being Nat st L = W -level n