theorem :: INT_2:7

- 1 is not Element of NAT ;