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