theorem Th1: :: NUMBER05:1

for n, k being Nat st n |^|^ k = 0 holds
n = 0