Topology of sequentially open sets is sequential? Let $(X,\tau)$ be a topological space.  The collection of all sequentially open subsets of $X$ (i.e. the complements of the sequentially closed subsets) is itself a topology $\tau_\text{seq}$, equal to $\tau$ if $X$ is a sequential space, and a strictly finer topology otherwise. (See the wikipedia article for details.)
Question: Is $(X,\tau_\text{seq})$ a sequential space?
 A: Suppose that $U$ is sequentially open with respect to $\tau_{\text{seq}}$, i.e., that every sequence converging in $\tau_{\text{seq}}$ to a point of $U$ is eventually in $U$. $\langle X,\tau_{\text{seq}}\rangle$ and $\langle X,\tau\rangle$ have the same convergent sequences, so $U$ is sequentially open with respect to $\tau$ and is therefore in $\tau_{\text{seq}}$. Thus, $\langle X,\tau_{\text{seq}}\rangle$ is sequential.
A: Preliminaries:
Define, for a sequence $(x_n)$ in $X$ the tail filter of the sequence by $$\textrm{tail}(x_n) = \{A \subseteq X\mid \exists m\in \Bbb N: \{x_n: n \ge m\} \subseteq A\}$$
The definition of convergence says in essence that $x_n \to x$ for any topology $\tau'$ on $X$ iff $$\{O \in \tau'\mid x \in O\} \subseteq \text{tail}(x_n)\tag{0}$$
It is standard that $\tau_{\text{seq}}$ is defined by all sets $O$ such that
$$\forall x \in O: \forall (x_n) \subseteq X: (x_n \to_\tau x) \to O \in \textrm{tail}(x_n)\tag{1}$$
which are called the sequentially open sets w.r.t. the topology $\tau$. The wikipedia page has a proof that this actually forms a topology on $X$ which clearly obeys $$\tau \subseteq \tau_{\text{seq}}$$ basically by the definition of convergence under $\tau$.

Proof
Now suppose that $O$ is sequentially open for $\tau_{\text{seq}}$. We have to show $O$ is actually in $\tau_{\text{seq}}$. So let $x \in O$ be arbitrary and $x_n \to_{\tau} x$.

Fact: $x_n \to x$ for $\tau_s$ as well: let $U$ be any open set in $\tau_{\text{seq}}$ containing $x$. Because $U \in \tau_{\text{seq}}$ and $x_n \to_\tau x$ by definition $U \in \textrm{tail}(x_n)$. But as $U \in \tau_{\text{seq}}$ was arbitrary containing $x$, indeed $x_n \to x$ for $\tau_{\text{seq}}$ ( we apply $(0)$ to $\tau_{\text{seq}}$) as required.

But as $O$ is sequentially open for $\tau_{\text{seq}}$, by definition again $O \in \textrm{tail}(x_n)$ and so $O$ (by $(1)$) is sequentially open for $\tau$,  i.e. $O \in \tau_{\text{seq}}$.
Which shows that $(X, \tau_{\text{seq}})$ is a sequential space by definition.
