theorem Th40: :: POLNOT_1:40

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
p = p ^ q )