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