theorem Th1: :: BINARI_4:1

for m being Nat st m > 0 holds
m * 2 >= m + 1