consider x being Element of X;
{x} in Fin X by FINSUB_1:def 5;
then reconsider s = {{x}} as Subset of (Fin X) by SUBSET_1:55;
take s ; :: thesis: s is with_non-empty_element
thus s is with_non-empty_element ; :: thesis: verum