for n being Nat
for x being object st x in Seg n holds
not not x = 1 & ... & not x = n by Lm5;