consider x being object such that
A1: x in D by XBOOLE_0:def 1;
reconsider x = x as Element of D by A1;
set S = {<*x*>};
for a being object st a in {<*x*>} holds
a is FinSequence of D by TARSKI:def 1;
then reconsider S = {<*x*>} as FinSequenceSet of D by FINSEQ_2:def 3;
take S ; :: thesis: ( not S is empty & S is with_non-empty_element )
thus ( not S is empty & S is with_non-empty_element ) ; :: thesis: verum