:: deftheorem Def4 defines Level TREES_2:def 4 :
for W being Tree
for b₂ being Subset of W holds
( b₂ is Level of W iff ex n being Nat st b₂ = { w where w is Element of W : len w = n } );