Let $\sigma_{\text{pullback}} \langle f \rangle$ be the
D1730: Pullback sigma-algebra on $X$ under $f$ with respect to $M_Y$. Result
R2548: Constant map pulls back a bottom sigma-algebra shows that $\sigma_{\text{pullback}} \langle f \rangle = \{ \emptyset, X \}$ and result
R4651: Bottom sigma-algebra is always a subsigma-algebra shows that
\begin{equation}
\sigma_{\text{pullback}} \langle f \rangle
= \{ \emptyset, X \}
\subseteq \mathcal{F}_X
\end{equation}
This establishes the result. $\square$
