consider x being Element of X;
take {x} ; :: thesis: ( {x} is finite & not {x} is empty )
thus ( {x} is finite & not {x} is empty ) ; :: thesis: verum