let k be natural number ; :: thesis: Seg k misses {(k + 1)}
assume not Seg k misses {(k + 1)} ; :: thesis: contradiction
then A1: (Seg k) /\ {(k + 1)} <> {} by XBOOLE_0:def 7;
consider x being Element of (Seg k) /\ {(k + 1)};
A2: x in Seg k by A1, XBOOLE_0:def 4;
then reconsider x = x as Element of NAT ;
x in {(k + 1)} by A1, XBOOLE_0:def 4;
then x = k + 1 by TARSKI:def 1;
then ( x <= k & k < x ) by A2, FINSEQ_1:3, XREAL_1:31;
hence contradiction ; :: thesis: verum