for n being Nat
for x being object st x in Segm (n + 1) holds
not not x = 0 & ... & not x = n