theorem Th7: :: NAT_1:7

for i, j being natural Number st i + j = 0 holds
( i = 0 & j = 0 )