theorem Th7: :: INT_3:7

for n being Nat st n > 0 holds
for a, b being Element of Segm n holds
( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )