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

proof

assume not Seg k misses {(k + 1)} ; :: thesis: contradiction
then A2: (Seg k) /\ {(k + 1)} <> {} by XBOOLE_0:def 7;
consider x being Element of (Seg k) /\ {(k + 1)};
A3: x in Seg k by A2, XBOOLE_0:def 4;
then reconsider x = x as Element of NAT ;
x in {(k + 1)} by A2, XBOOLE_0:def 4;
then A4: x = k + 1 by TARSKI:def 1;
x <= k by A3, Th3;
hence contradiction by A4, XREAL_1:31; :: thesis: verum

end;

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