:: deftheorem defines Seg FINSEQ_1:def 1 :
for n being natural Number holds Seg n = { k where k is Nat : ( 1 <= k & k <= n ) } ;