$P$ poset: $ J \subseteq P$ is join-dense iff $\forall x \in P$, $\,\,\, x = (\downarrow x \cap J) $

Question

Let $\mathrm{P}$ be a poset: $ \mathrm{J} \subseteq \mathrm{P}$ is join-dense in $\mathrm{P} \iff \forall x\in \mathrm{P}$ we have $x =\bigvee (\downarrow x\cap \mathrm{J})$

about this implication "$\Rightarrow$", since $\mathrm{J}$ is join-dense in $\mathrm{P}$, $\exists\,\, \mathrm{S} \subseteq\mathrm{J}$ s.t. $x = \lor \mathrm{S}$, so I am trying so show that $\mathrm{S} = \downarrow x\cap\mathrm{J}$: $\,\,$let $b\in\mathrm{S} \Rightarrow$ $b \le \lor\mathrm{S} = x$, so $b \in \downarrow x \Rightarrow b\in \downarrow x\cap\mathrm{J}$. $\,\,\,\,$ Now let $c \in \mathrm{I}\cap\mathrm{J}$ $\Rightarrow c \le x = \lor \mathrm{S}$ $\,\,\,\,(...)$

any idea how to complete it? Or maybe there is a different path to follow?

The implication $"\Leftarrow"$ is easy because of the assumption, by putting $T := \downarrow x \cap J \subseteq J$, then $\forall x \in P \,\, \exists \,\, T \subseteq J$ s.t.$\,\, x= \bigvee T$, that is the definition of join-dense set.

Answer 1

It is very easy.

Since $J$ is join-dense in $P$, for every $x \in P$ there exists $A \subseteq J$ such that $x = \bigvee A$.
(This is just the definition of join-dense set.)

In these conditions, it is clear that $A \subseteq {\downarrow}x$. Thus we can take $A$ to be ${\downarrow}x \cap J$, and obtain $x = \bigvee ({\downarrow}x \cap J)$.