set x = the non empty Element of X;
take IT = { the non empty Element of X}; :: thesis: IT is with_non-empty_elements
thus IT is with_non-empty_elements ; :: thesis: verum