Existence of a converging sequence in the subspace P.S: see the comment for more specification
This is a reduced version of something that I read and thought that should be trivial, but I couldn't get the formalism correctly.

Let $X$ be a topological space, $Y\subset X$ a subspace. Suppose that there is $x_0\in X$ such that for every $x_0\in U\subset X$ open there is $y_U\in Y\cap U$. 
  Prove that there is a sequence $y_n\in Y$ with $y_n\to x_0$

This seems trivial, as every neighborhood of $x_0$ has a member of $Y$, but I couldn't write a formal constructions of such sequence as it is possible that there are more than $\mathbb N$ different neighborhoods of $x_0$.
In case this is just not a correct proposition:


*

*Would it help if $X$ was locally compact?

*Would it help if $X$ was a locally compact topological group and $Y$ a discrete subgroup?

 A: This is not true in general, even if $X$ is compact Hausdorff.  For instance, if $X=[0,1]^I$ for an uncountable set $I$, and $Y$ is the subspace of elements that are $0$ on all but finitely many coordinates, then $Y$ dense in all of $X$ but any limit of a sequence in $Y$ can be nonzero on only countably many coordinates.
It is true if $X$ is a locally compact group and $Y$ is a discrete subgroup, because then your hypotheses actually imply $x_0\in Y$ (that is, $Y$ is closed).  Indeed, suppose $x_0\not\in Y$ and let $V$ be any neighborhood of $1$.    Since $x_0x_0^{-1}=1$, there is a neighborhood $U$ of $x_0$ such that for any $a,b\in U$, $ab^{-1}\in V$.  Choose $y\in Y\cap U$.  Since $x_0\not\in Y$, $y\neq x_0$, so $U\setminus\{y_0\}$ is still a neighborhood of $x_0$, so we can also choose $z\in Y\cap U\setminus\{y_0\}$.  Then $yz^{-1}\in V\setminus\{1\}$, and also $yz^{-1}\in Y$.
Thus every neighborhood of $1$ contains a point from $Y$ other than $1$.  This means that $1$ is not an isolated point of $Y$, which contradicts the assumption that $Y$ is discrete.
