let k be natural Number ; :: 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;
the Element of (Seg k) /\ {(k + 1)} in {(k + 1)} by A2, XBOOLE_0:def 4;
then the Element of (Seg k) /\ {(k + 1)} = 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