not 0 in Seg n by FINSEQ_1:1;
hence Seg n is with_non-empty_elements by SETFAM_1:def 8; :: thesis: verum