theorem :: POLNOT_1:42

for P being FinSequence-membered set
for a being object st P = {a} holds
P is antichain-like ;