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: s is with_non-empty_element
thus s is with_non-empty_element ; :: thesis: verum