How to prove this sequent by natural deduction?

Question

How do I prove

$$\exists x\exists y(S(x,y)\lor S(y,x))\vdash\exists x\exists y S(x,y)$$

by natural deduction?

I've written follows:

1$\quad\quad\exists x\exists y(S(x,y)\lor S(y,x))\quad$ assumption

2$\quad x_0$

3$\quad\quad\exists y(S(x_0,y)\lor S(y,x_0))\quad$ assumption

4$\quad y_0$

5$\quad\quad S(x_0,y_0)\lor S(y_0,x_0)\quad$ assumption

And I stuck here. Can somebody give me some advice? Thanks a lot.

I got the hint, is this right:

Answer 1

Case I $S(x_{0},y_{0})$. Then $\exists y S(x_{0},y)$, so $\exists x\exists y S(x,y)$, done.

Case II $S(y_{0},x_{0})$. Then $\exists y S(y_{0},y)$, so $\exists x\exists yS(x,y)$, done.

Answer 2

Hint

From 5) we need $\lor$-elim (or Disjunction elimination):

5a) From $S(x_0,y_0)$ we derive $\exists x \exists y S(x,y)$ by $\exists$-intro twice.

5b) From $S(y_0,x_0)$ we derive $\exists x \exists y S(x,y)$ by $\exists$-intro twice.