theorem :: NAT_1:45

for n being natural Number holds n in Segm (n + 1)