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