:: deftheorem defines -level TREES_2:def 6 :
for W being Tree
for n being Nat holds W -level n = { w where w is Element of W : len w = n } ;