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