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