theorem :: TREES_2:10

for W being Tree
for w being Element of W holds succ w is AntiChain_of_Prefixes of W