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