theorem Th11: :: NAT_1:11

for i, j being natural Number holds i <= i + j