Dgdrxrt

The next problem appears in the book "Real analysis" by Thomson/Bruckner in the chapter of Integrable functions. My proof seems good to me but I'm not confident enough with my proofs in this subject.
Here, $(X, sigma, mu)$ is a measurable space. I use the following:

Definition
Given a succession $(E_n)$ of measurable sets, $limsup E_n = x in X : x$ belongs to $E_j$ for infinitely many $j $

Theorem: if $(E_n)$ is a succession of measurable sets and $mu (cup E_n) < infty$ then $limsup mu(E_n) leq mu(limsup E_n)$

Problem: Suppose that $f in L_1(X)$, that $f(x)>0$ for all $x in X$, and that $0 < alpha < mu(X) < infty $. Prove that
$$ inf left int_E f dmu : mu (E) geq alpharight > 0. $$

My attempt:

Suppose that $inf left int_E f dmu : mu (E) geq alpharight = 0$. Then, we can choose a succession $(E_n)_n geq 1$ such that $mu(E_n) geq alpha$ and
$$ int_En f < fracalpha2^n.$$
Then, $f|_E_n < frac12^n $. For if $f|_E_n geq frac12^n $ then we have
$$ fracalpha2^n > int_E_n f d mu geq int_E_n fracd mu2^n = fracmu(E_n)2^n geq fracalpha2^n,$$
a contradiction.

Now, if there exist $ x in X$ such that $x in limsup E_n$ then $f(x)<fracalpha2^j$, for infinitely many $j's$. So we must have $f(x) = 0$, contradicting that $f > 0$. Therefore $limsup E_n = emptyset$ and $mu (limsup E_n)=0$.
However
$limsup mu(E_n) geq alpha$ because $mu(E_n) geq alpha$ for every $n$. And because we are in a space of finite measure, we can aply the above theorem and obtain
$$ 0 < alpha leq limsup mu(E_n) leq mu (limsup E_n) = 0. $$
So $alpha = 0$ is our final contradiction.

For $ninmathbbN$, define $A_n=x:f(x)>frac1n$ note that $A_nuparrow X$ (because $f(x)>0$), so $mu(A_n)uparrowmu(X)$. Hence, there is some $m$ big enough such that $mu(X)-mu(A_m)=mu(X-A_m)<alpha/2$.

Therefore, for any set $E$ with $mu(E)>alpha$, you will have that $mu(Ecap A_m)geq mu(E)-mu(X-A_m)>fracalpha2$.

Hence, $int_Ef dmugeq int_Ecap A_mf dmugeqint_Ecap A_mfrac1mdmu=frac1mmu(Ecap A_m)>fracalpha2m$.

So the infimum is at least $fracalpha2m>0$.