let Y be Subset of X; :: thesis: Y is with_non-empty_elements
not {} in Y ;
hence Y is with_non-empty_elements by SETFAM_1:def 8; :: thesis: verum