let k be Nat; :: thesis: (Seg (k + 1)) \ (Seg k) = {(k + 1)}
A1: Seg (k + 1) = (Seg k) \/ {(k + 1)} by FINSEQ_1:9;
Seg k misses {(k + 1)} by Th14;
hence (Seg (k + 1)) \ (Seg k) = {(k + 1)} by A1, XBOOLE_1:88; :: thesis: verum