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