theorem Th10: :: LIOUVIL1:8

for d being Integer ex n being non zero Nat st 2 to_power (n - 1) > d