theorem Th3: :: CALCUL_2:3

for a, b being Nat holds
( b = 0 or b + a in seq (a,b) )