theorem Th8: :: AMISTD_1:8

for z being Nat
for N being with_zero set
for l being Nat st l = z holds
SUCC (l,(STC N)) = {z,(z + 1)}