set P = {<* the set *>};
for a being object st a in {<* the set *>} holds
a is FinSequence by TARSKI:def 1;
then reconsider P = {<* the set *>} as non empty FinSequence-membered set by FINSEQ_1:def 19;
take P ; :: thesis: P is antichain-like
thus P is antichain-like ; :: thesis: verum