for n, k being Nat holds
( k in Segm n iff k + 1 in Seg n ) by Th2, NAT_1:44;