Tweak for T420 (T2 => semi-Hausdorff)

properties/P000010.md

@@ -6,6 +6,7 @@ refs:
     name: General Topology (Willard)
 ---
 
-A space with a basis $\mathcal{B}$ of open sets such that $\operatorname{int}(\operatorname{cl}(O)) = O$ for every $O \in \mathcal{B}$.
+A space with a base $\mathcal{B}$ of regular open sets, that is,
+$\operatorname{int}(\operatorname{cl}(O)) = O$ for every $O \in \mathcal{B}$.
 
 Defined in 14E of {{zb:1052.54001}}.

theorems/T000420.md

@@ -11,8 +11,7 @@ refs:
     name: "Reference search: separation by regular open sets"
 ---
 
-Assume $x,y$ are separated by the disjoint open sets $U,V$. Let $U_{r}=int(cl(U))$ be regular open.
-It follows that $U\cap V=\emptyset$ implies $cl(U)\cap V=\emptyset$,
-since no point of $V$ may be a limit point of $U$.
-Therefore $U_{r}\cap V=int(cl(U))\cap V=\emptyset$;
-in particular, $x\in U_r$ and $y\not\in U_r$.
+Assume the points $x,y$ are separated by disjoint open sets $U$ and $V$.
+Then $\operatorname{cl}(U)\cap V=\emptyset$.
+The set $U'=\operatorname{int}(\operatorname{cl}(U))$ is regular open
+and satisfies $x\in U\subseteq U'$ and $U'\cap V = \emptyset$, so that $y\notin U'$.