SegM n c= NAT ;
hence SegM n is Subset of NAT ; :: thesis: verum