for k, n being Nat st k <= n holds
not not k = 0 & ... & not k = n