theorem :: FINSEQ_3:15

for k being Nat holds (Seg (k + 1)) \ (Seg k) = {(k + 1)}