Under choice, a regular $T_1$ space with a $\sigma$-locally-finite basis has a compatible normal sequence

Assume the Axiom of Choice. A regular $T_1$ space with a $\sigma$-locally-finite basis has a compatible normal sequence of open covers.

Source convention. In Granath's source, regularity is defined only for a Fréchet space, i.e. a $T_1$ space. The displayed library statement therefore names $T_1$ separately rather than silently importing that convention.

Not proved in this library. This is a source-backed fallback rather than a local proof. The discarded local route chose a shrinking $W(B,x)$ for every point of every basis member and claimed that its families stayed locally finite. That claim is false: with $X=B=\mathbb R$ and the one-member locally finite family $\{B\}$, the allowed shrinkings $W(B,x)=(x-1,x+1)$ have infinite local overlap at every point. The standard normal-cover construction needs additional machinery beyond that failed pointwise shrinking.

Why it remains visible. The Nagata--Smirnov comparison below depends on exactly this standard route. Its dependency marker therefore records that the result is externally sourced rather than pretending that the invalid local construction proves it.