let X be AntiChain_of_Prefixes of T; :: thesis: X is finite
X c= T by Def14;
hence X is finite ; :: thesis: verum