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$