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