How to prove that Supremum preorder coincides with Hoare preorder? Given a complete lattice $(L, \sqsubseteq)$ and a basis of completely $\sqcup$-irreducibles $B_L \subseteq L$, such that $\forall l \in L$, $l=\sqcup\{b \in B_L\ |\ b \sqsubseteq l\}$.

I mean:


Hoare preorder $(2^{B_L}, \sqsubseteq_H)$, where for $X, Y \in 2^{B_L}$, 

$X \sqsubseteq_H Y \iff \forall x \in X$, $\exists y \in Y$ such that $x \sqsubseteq y$
Supremum preorder $(2^{B_L}, \sqsubseteq_{\sqcup})$, where for $X, Y \in 2^{B_L}$, 

$X \sqsubseteq_{\sqcup} Y \iff \sqcup X \sqsubseteq \sqcup Y$


Where $l \in L$ is completely $\sqcup$-irreducibles $\iff \forall X' \subseteq L$ such that $l = \sqcup X' \implies l \in X'$ (note that $\bot$ isn't completely $\sqcup$-irreducible since $\bot = \sqcup \emptyset$ but $\bot \not\in \emptyset$).

I'm pretty sure that "Hoare" is the right name for the intended preorder, a little less about "Supremum" (maybe "Smyth" could be better).

My question is, given a distributive lattice $L$, how to prove that Hoare preorder and Supremum preorder coincide?
It is easy to see that in general (without distributivity) $X \sqsubseteq_H Y \implies X \sqsubseteq_{\sqcup} Y$. But I'm stuck in the converse implication $X \sqsubseteq_{\sqcup} Y \implies X \sqsubseteq_H Y$, that probably uses distributivity of $L$.

Where $L$ is distributive $\iff \forall a, b, c \in L$ it holds that $a \sqcap (b \sqcup c) = (a \sqcap b) \sqcup (a \sqcap c)$. By the way, I'm still not sure if I need to require $L$ to be only distributive or completely distributive.

Thanks in advance for any hint.
I’m going to use normal notation, as the square symbols are a pain to typeset.

Proposition: Let $L$ be a complete lattice, and $B$ its set of completely join-irreducible elements. If every element of $L$ is a join of a subset of $B$, then the following are equivalent:

$\bigvee X\le\bigvee Y\implies \forall x\in X\,\exists y\in Y\,x\le y$ for all $X,Y\subseteq B$.

All $x\in B$ are completely join-prime, i.e., $x\le\bigvee Y\implies\exists y\in Y\,x\le y$ for all $Y\subseteq L$.

$L$ satisfies the infinitary distributive law $x\land\bigvee_{i\in I}y_i=\bigvee_{i\in I}(x\land y_i)$.



Note that condition 3 is not equivalent to its dual, and it is weaker than full complete distributivity.
Proof:
1 → 2: By the assumption on $L$, $\bigvee Y=\bigvee\{u\in B:\exists y\in Y\,u\le y\}$. Thus, if $x\le\bigvee Y$, then $\bigvee\{x\}\le\bigvee\{u\in B:\exists y\in Y\,u\le y\}$, hence by 1, there exists $u\in B$ and $y\in Y$ such that $x\le u\le y$.
2 → 1: For any $x\in X$, $x\le\bigvee X\le\bigvee Y$, hence $x\le y$ for some $y\in Y$ as $x$ is completely join-prime.
3 → 2: If $x$ is completely join-irreducible and $x\le\bigvee Y$, then $x=\bigvee\{x\land y:y\in Y\}$ by 3, hence $x=x\land y$ (i.e., $x\le y$) for some $y\in Y$ by complete irreducibility.
2 → 3: $x\land\bigvee_{i\in I}y_i\ge\bigvee_{i\in I}(x\land y_i)$ always holds. For the other inequality, since the left-hand side is a join of a subset of $B$ by assumption, it suffices to show that
$$u\le x\land\bigvee_{i\in I}y_i\implies u\le\bigvee_{i\in I}(x\land y_i)$$
for all $u\in B$. The premise implies $u\le x$, and since $u$ is completely join-prime by 2, there exists $i\in I$ such that $u\le y_i$. Then $u\le x\land y_i\le\bigvee_{i\in I}(x\land y_i)$.