take cobool X ; :: thesis: cobool X is with_empty_element
thus cobool X is with_empty_element ; :: thesis: verum