theorem :: NEWTON02:106

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