theorem Th2: :: NUMBER08:2

NATPLUS = NAT \ {0}