theorem :: TREES_2:9

for W being Tree
for L being Level of W holds L is AntiChain_of_Prefixes of W