theorem :: NAT_1:61

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