for n being Nat holds succ (Segm n) = { l where l is Nat : l <= n }