let X be non empty set ; :: thesis: not for Y being Finite_Subset of holds Y is empty
consider a being Element of X;
{.a.} is Finite_Subset of ;
hence not for Y being Finite_Subset of holds Y is empty ; :: thesis: verum