theorem :: ASYMPT_1:65

for n being Element of NAT st n >= 4 holds
(2 * n) + 3 < 2 to_power n by Lm7;