ThmDex – An index of mathematical definitions, results, and conjectures.
P3096
By definition \begin{equation} \text{int} \langle U \rangle : = \bigcup \{ V \in \mathcal{T} : V \subseteq U \} \end{equation} Result R125: Subset relation is reflexive shows that $U$ itself satisfies $U \subseteq U$. Since $U$ is also an open set, then $U$ is a set in the union $\text{int} \langle U \rangle$ and result R4142: Union is an upper bound to each set in the union implies that $U \subseteq \text{int} \langle U \rangle$.

Conversely, result R3945: Set is a superset to its interior guarantees that $\text{int} \langle U \rangle \subseteq U$. Since we have inclusions in both directions, the claim then follows as a consequence of R2741: Set equality iff inclusion in both directions. $\square$