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-membered
thus not s is empty-membered ; :: thesis: verum