theorem Th1: :: TURING_1:1

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