- n is not Element of NAT by Th8;
hence not - n is natural by ORDINAL1:def 13; :: thesis: verum