let n be Nat; :: thesis: succ (Segm n) = { l where l is Nat : l <= n }
thus succ (Segm n) c= { k where k is Nat : k <= n } :: according to XBOOLE_0:def 10 :: thesis: { l where l is Nat : l <= n } c= succ (Segm n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in succ (Segm n) or x in { k where k is Nat : k <= n } )
assume A1: x in succ (Segm n) ; :: thesis: x in { k where k is Nat : k <= n }
then x in Segm (succ (Segm n)) ;
then reconsider k = x as Nat ;
( x in Segm n or x in {n} ) by A1, XBOOLE_0:def 3;
then ( k < n or k = n ) by Th32, TARSKI:def 1;
hence x in { k where k is Nat : k <= n } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Nat : l <= n } or x in succ (Segm n) )
assume x in { k where k is Nat : k <= n } ; :: thesis: x in succ (Segm n)
then consider k being Nat such that
A2: x = k and
A3: k <= n ;
( k < n or k = n ) by A3, XXREAL_0:1;
then ( k in Segm n or k in {n} ) by Th32, TARSKI:def 1;
hence x in succ (Segm n) by A2, XBOOLE_0:def 3; :: thesis: verum