let n be natural Number ; :: thesis: n in Segm (n + 1)
A1: n is Nat by TARSKI:1;
n < n + 1 by XREAL_1:29;
then n in { l where l is Nat : l < n + 1 } by A1;
hence n in Segm (n + 1) by AXIOMS:4; :: thesis: verum