theorem Th9: :: HILB10_8:9

for n being Nat
for T being _Theta
for alpha, epsilon being Real st alpha = (1 + (T * epsilon)) |^ n & 0 <= epsilon & epsilon <= 1 / (2 * n) holds
ex T1 being _Theta st alpha = 1 + (((T1 * 2) * n) * epsilon)