:: deftheorem Def16 defines antichain-like POLNOT_1:def 16 :
for P being FinSequence-membered set holds
( P is antichain-like iff for p, q being FinSequence st p in P & p ^ q in P holds
q = {} );