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