for n, k being Nat holds
( k in SegM n iff k <= n )