Yoneda embedding and representation of partial order set

Let $(P,\le )$$(P,\le)$ be a partial order set, hence a category.

We can embed $(P,\le )$$(P,\le)$ into $(2^P,\subseteq )$$(2^P,\subseteq)$ by consider

$$\begin{array}{}\text{(1)}& a⟼a\downarrow \end{array}$$

here $a\downarrow$$a\downarrow$ is $\{x\in P|x\le a\}$$\{x\in P|x\le a\}$.

Hence we have :

$$\begin{array}{}\text{(2)}& a\le b⟺a\downarrow \subseteq b\downarrow \end{array}$$

Proof.

$\Rightarrow$$\Rightarrow$ is obvious. If $a\downarrow \subseteq b\downarrow$$a\downarrow\subseteq b\downarrow$, by definition, $a\in a\downarrow \subseteq b\downarrow ⟹a\le b$$a\in a\downarrow\subseteq b\downarrow\implies a\le b$. $◻$$\square$

Indeed, this is just an application of Yoneda embedding. Here $a\downarrow$$a\downarrow$ correspond to ${\mathrm{Hom}}_P(-,a)$$\mathrm{Hom}_{P}(-,a)$