theorem :: TREES_2:13

for W being Tree
for w being Element of W st w = {} holds
W -level 1 = succ w