let k be Nat; :: thesis: not k + 1 in Seg k
assume k + 1 in Seg k ; :: thesis: contradiction
then A1: k + 1 <= k by FINSEQ_1:1;
k <= k + 1 by NAT_1:12;
then k + 0 = k + 1 by A1, XXREAL_0:1;
hence contradiction ; :: thesis: verum