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