theorem Th7: :: NUMBER02:7

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