n is Element of NAT by ORDINAL1:def 13;
hence SegM n is finite by CQC_THE1:12; :: thesis: not SegM n is empty
0 <= n by NAT_1:2;
then 0 in { k where k is Element of NAT : k <= n } ;
hence not SegM n is empty ; :: thesis: verum