Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that

(i)	$f : X \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$

Let $\lambda \in (0, \infty)$ be a D5407: Positive real number.

Since $f$ is nonzero then, by construction, one has the pointwise inequality \begin{equation} \lambda I_{\{ f \geq \lambda \}} \leq f \end{equation} Result R1214: Isotonicity of unsigned basic integral allows us to integrate each side and preserve the inequality, while result R1213: Linearity of unsigned basic integral allows us to factor the constant $\lambda > 0$ out of the integral. We obtain \begin{equation} \lambda \int_X I_{\{ f \geq \lambda \}} \, d \mu \leq \int_X f \, d \mu \end{equation} Applying now R1242: Unsigned basic integral is compatible with measure on the left hand side, we conclude \begin{equation} \lambda \mu( f \geq \lambda) = \lambda \int_X I_{\{ f \geq \lambda \}} \, d \mu \leq \int_X f \, d \mu \end{equation} The result then follows by multiplying each side by the constant $1 / \lambda$. $\square$