:: deftheorem defines seq CALCUL_2:def 1 :
for m, n being Nat holds seq (m,n) = { k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } ;