consider X being with_non-empty_element set ;
take X ; :: thesis: X is with_non-empty_element
thus X is with_non-empty_element ; :: thesis: verum