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