{} is not Element of m1 -tuples_on U ;
hence m1 -tuples_on U is with_non-empty_elements by SETFAM_1:def 8; :: thesis: verum