theorem :: NAT_1:54

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