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