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