theorem :: FINSEQ_1:10

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