set x = the Element of X;
{ the Element of X} in Fin X by FINSUB_1:def 5;
then reconsider s = {{ the Element of X}} as Subset of (Fin X) by SUBSET_1:33;
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 8 :: thesis: contradiction
hence contradiction ; :: thesis: verum