take { the non empty Element of X} ; :: thesis: ( { the non empty Element of X} is with_non-empty_elements & not { the non empty Element of X} is empty )
thus ( { the non empty Element of X} is with_non-empty_elements & not { the non empty Element of X} is empty ) ; :: thesis: verum