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: ( not s is empty & s is with_non-empty_elements )
thus not s is empty ; :: thesis: s is with_non-empty_elements
assume {} in s ; :: according to SETFAM_1:def 9 :: thesis: contradiction
hence contradiction ; :: thesis: verum