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