n is Element of NAT by ORDINAL1:def 13;
hence SegM n is finite by CQC_THE1:12; :: thesis: not SegM n is empty
thus not SegM n is empty ; :: thesis: verum