Par définition du spectre (analytique) d’une algèbre affinoïde, il existe une fonction holomorphe $f$ sur $X$ telle que $\mathopen{|}{f(x)}\mathclose{|}\neq\mathopen{|}{f(y)}\mathclose{|}$.

Supposons ces deux valeurs non nulles  ; soit $\varphi$ une fonction $\mathscr{C}^{\infty}$ à support compact sur $\mathbf{R}$ valant $0$ au voisinage de $\log\mathopen{|}{f(x)}\mathclose{|}$ et $1$ au voisinage de $\log\mathopen{|}{f(y)}\mathclose{|}$. La fonction $\varphi\circ\log\mathopen{|}{f}\mathclose{|}$, définie sur l’ouvert d’inversibilité de $f$, est lisse ; prolongeons-la par $0$ sur $X$ tout entier. Comme $\varphi$ est à support compact, la fonction obtenue est nulle au voisinage de l’ensemble des zéros de $f$ ; elle est donc lisse.

Si $f(x)=0$, on raisonne de même à partir d’une fonction $\varphi$ à support compact valant $1$ au voisinage de $\log\mathopen{|}{f(y)}\mathclose{|}$.

Si $f(y)=0$, on construit comme ci-dessus une fonction lisse $u$ qui est nulle au voisinage de $y$ et qui vaut $1$ au voisinage de $x$ ; la fonction $1-u$ convient. ∎