SegM n in NAT by ORDINAL1:def 13;
then SegM n c= NAT by ORDINAL1:7;
hence SegM n is Subset of NAT ; :: thesis: verum