for X being non empty set holds
not for Y being Element of Fin X holds Y is empty