theorem Th32: :: NAT_1:44

for k, n being natural Number holds
( k in Segm n iff k < n )