theorem Th12: :: BINARI_4:12

for n being non zero Nat
for z being Tuple of n, BOOLEAN st z /. n = TRUE holds
Absval z >= 2 to_power (n -' 1)