:: deftheorem Def2 defines Segm0 INT_7:def 2 :
for n being Nat st 1 < n holds
Segm0 n = (Segm n) \ {0};