let k be Nat; :: thesis: Seg k = (Seg (k + 1)) \ {(k + 1)}
A1: Seg (k + 1) = (Seg k) \/ {(k + 1)} by Th9;
Seg k misses {(k + 1)}

proof

assume not Seg k misses {(k + 1)} ; :: thesis: contradiction
then A2: (Seg k) /\ {(k + 1)} <> {} ;
set x = the Element of (Seg k) /\ {(k + 1)};
A3: the Element of (Seg k) /\ {(k + 1)} in Seg k by A2, XBOOLE_0:def 4;
then reconsider x = the Element of (Seg k) /\ {(k + 1)} as Element of NAT ;
x in {(k + 1)} by A2, XBOOLE_0:def 4;
then x = k + 1 by TARSKI:def 1;
hence contradiction by A3, Th1, XREAL_1:29; :: thesis: verum

end;

hence Seg k = (Seg (k + 1)) \ {(k + 1)} by A1, XBOOLE_1:88; :: thesis: verum