:: deftheorem Def10 defines AntiChain_of_Prefixes-like TREES_1:def 10 :
for IT being set holds
( IT is AntiChain_of_Prefixes-like iff ( ( for x being set st x in IT holds
x is FinSequence ) & ( for p1, p2 being FinSequence st p1 in IT & p2 in IT & p1 <> p2 holds
not p1,p2 are_c=-comparable ) ) );