:: deftheorem defines SegM TURING_1:def 1 :
for n being Nat holds SegM n = { k where k is Nat : k <= n } ;