let L be Subset of A; :: thesis: L is with_non-empty_elements
not 0 in L ;
hence L is with_non-empty_elements by SETFAM_1:def 8; :: thesis: verum