let k be natural number ; :: thesis: not k + 1 in Seg k
assume k + 1 in Seg k ; :: thesis: contradiction
then ( k + 1 <= k & k <= k + 1 ) by FINSEQ_1:3, NAT_1:12;
then k + 0 = k + 1 by XXREAL_0:1;
hence contradiction ; :: thesis: verum