Coproduct of bounded distributive lattices given as lattices of subsets Let $X$ be a set. A lattice of subsets of $X$ is a subset of
$\mathcal{P}(X)$ containing $\emptyset$ and $X$ and closed under finite
intersection and finite union. Such a lattice is therefore a bounded distributive lattice.
Let $X_0$ and $X_1$ be sets. Let $\mathcal{L}_0$  be a lattice of subsets of $X_0$ and let $\mathcal{L}_1$ be a lattice of subsets of $X_1$. Let $\mathcal{L}$ be the lattice of subsets of $X_0 \times X_1$ consisting of the finite unions of sets of the form $L_0 \times L_1$ with $L_0 \in \mathcal{L}_0$ and $L_1 \in \mathcal{L}_1$. 
Question. Is $\mathcal{L}$ (isomorphic to) the coproduct of $\mathcal{L_0}$ and $\mathcal{L_1}$ in the category of bounded distributive lattices?
If the answer is positive, a reference would be appreciated.
 A: The answer is yes. Unfortunately, I don't have a reference.
Allow me to change notations to talk about $\mathcal L \subseteq \mathcal{P}(X)$ and $\mathcal M \subseteq \mathcal{P}(Y)$. Denote by $\mathcal L \otimes \mathcal M \subset \mathcal P(X \times Y)$ the sublattice generated by $\{L \times M \mid L \in \mathcal L, M \in \mathcal M\}$. The goal is to show that $\mathcal L \otimes \mathcal M$ is the coproduct of $\mathcal L$ and $\mathcal M$, with the structure maps $\mathcal L \to \mathcal L \otimes \mathcal M$, $L \mapsto L \times Y$ and $\mathcal M \to \mathcal L \otimes \mathcal M$, $M \mapsto X \times M$. 
We verify the universal property directly. Given lattice homomorphisms $\mathcal L \overset{\phi}{\to} \mathcal P \overset{\psi}{\leftarrow} \mathcal M$, it's easy to see that a lattice homomorphism $[\phi,\psi]: \mathcal L \otimes \mathcal M \to \mathcal P$ commuting with the structure maps must satisfy $[\phi,\psi](\cup_{i \in I} L_i \times M_i) = \vee_i \phi(L_i) \wedge \psi(M_i)$ (using the fact that $L \times M = L \times Y \cap X \times M$); we're done as soon as we can show that this defines a lattice homomorphism. The only verification which is not straightforward is to see that this is actually a function.
So suppose that $\cup_{i \in I} L_i \times M_i = \cup_{j \in J} L_j \times M_j$ where without loss of generality all of the $L_i$'s, $L_j$'s, $M_i$'s, and $M_j$'s are nonempty. We want to show that $[\phi,\psi]( \cup_{i \in I} L_i \times M_i) = [\phi,\psi](\cup_{j \in J} L_j \times M_j)$. It will suffice to show that $[\phi,\psi](\cup_{i \in I} L_i \times M_i) = [\phi,\psi](\cup_{(i,j) \in I \times J} L_i \cap L_j \times M_i \cap M_j)$. This follows from the fact that
(*) For each $i \in I$, $L_i = \cup_{j \in J} L_i \cap L_j$ and $M_i = \cup_{j \in J} M_i \cap M_j$
For then
$[\phi,\psi](\cup_{i \in I} L_i \times M_i) = \vee_{i \in I} \phi(L_i) \wedge \psi(M_i) = \vee_{i \in I} \phi(\cup_{j \in J} L_i \cap L_j) \wedge \psi(\cup_{j \in J} M_i \cap M_j) \\
\qquad \qquad \qquad \quad = \vee_{i \in I} \vee_{j \in J} \phi(L_i \cap L_j) \wedge \vee_{j \in J} \psi(M_i \cap M_j) = \vee_{(i,j) \in I \times J} \phi(L_i \cap L_j) \wedge \psi(M_i \cap M_j) \\
\qquad \qquad \qquad \quad = [\phi,\psi](\cup_{(i,j) \in I \times J} L_i \cap L_j \times M_i \cap M_j)$
as desired.
Proof of (*). Suppose there is $i \in I$ such that $\cup_{j \in J} L_i \cap L_j \subsetneq L_i$. Then there is $l \in L_i$ such that $l \not\in L_j$ for any $j \in J$. Take some $m \in M_i$. Then $(l,m) \in \cup_{i \in I} L_i \times M_i$, but $(l,m) \not \in \cup_{i \in I} L_i\cap L_j \times M_i \cap M_j$ because every $\mathcal L$-coordinate of a point in the latter is certainly in $\cup_j L_j$.
