theorem :: TREES_2:11

for W being Tree
for A being AntiChain_of_Prefixes of W
for C being Chain of W ex w being Element of W st A /\ C c= {w}