let k be natural number ; :: thesis: (Seg (k + 1)) \ (Seg k) = {(k + 1)}
A1: Seg (k + 1) = (Seg k) \/ {(k + 1)} by FINSEQ_1:11;
Seg k misses {(k + 1)} by Th15;
hence (Seg (k + 1)) \ (Seg k) = {(k + 1)} by A1, XBOOLE_1:88; :: thesis: verum