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