{} in {{}} by TARSKI:def 1;
then not {} in X \ {{}} by XBOOLE_0:def 5;
hence X \ {{}} is with_non-empty_elements by SETFAM_1:def 8; :: thesis: verum