let n be Nat; :: thesis: succ (Segm n) = Segm (n + 1)
A1: n + 1 = { L where L is Nat : L < n + 1 } by AXIOMS:4;
A2: n = { K where K is Nat : K < n } by AXIOMS:4;
thus succ (Segm n) c= Segm (n + 1) :: according to XBOOLE_0:def 10 :: thesis: Segm (n + 1) c= succ (Segm n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in succ (Segm n) or x in Segm (n + 1) )
assume A3: x in succ (Segm n) ; :: thesis: x in Segm (n + 1)

per cases ( x in Segm n or x = n ) by A3, ORDINAL1:8;

suppose x in Segm n ; :: thesis: x in Segm (n + 1)

then consider K being Nat such that
A4: x = K and
A5: K < n by A2;
K < n + 1 by A5, Th13;
hence x in Segm (n + 1) by A1, A4; :: thesis: verum

end;

suppose A6: x = n ; :: thesis: x in Segm (n + 1)

reconsider n = n as Element of NAT by ORDINAL1:def 12;
n < n + 1 by Th13;
hence x in Segm (n + 1) by A1, A6; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Segm (n + 1) or x in succ (Segm n) )
assume x in Segm (n + 1) ; :: thesis: x in succ (Segm n)
then consider K being Nat such that
A7: x = K and
A8: K < n + 1 by A1;
K <= n by A8, Th13;
then ( K = n or K < n ) by XXREAL_0:1;
then ( x = n or x in Segm n ) by A2, A7;
hence x in succ (Segm n) by ORDINAL1:8; :: thesis: verum