Solution (source code)

= Solution

If the origin had a <first-countable space>[countable local basis] $U_1,U_2,\ldots$, replace it by the decreasing <first-countable space>[local basis] $V_n=\bigcap_{j\le n}U_j$. Each $V_n$ meets the <dense set> $Y$, so choose $p_n\in V_n\cap Y$. Given any <neighbourhood> $U$ of the origin, some $U_j$ is contained in $U$; for every $n\ge j$ we then have $p_n\in V_n\subseteq U_j\subseteq U$. Thus $p_n$ converges to the origin, contradicting the preceding part. Consequently \b[<first countability> fails already at the origin], and $X$ is not <first countable>.