:: deftheorem defines antichain-like POLNOT_1:def 17 :
for D being non empty set
for G being Subset of (D *) holds
( G is antichain-like iff for g, h being FinSequence of D st g in G & g ^ h in G holds
h = <*> D );