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