I’ve proved a new simple proposition about infimum product:
Theorem
Let $latex \pi^X_i$ be metamonovalued morphisms. If $latex S \in \mathscr{P} (
\mathsf{FCD} ( A_0 ; B_0) \times \mathsf{FCD} ( A_1 ; B_1))$
for some sets $latex A_0$, $latex B_0$, $latex A_1$, $latex B_1$ then
$latex \bigsqcap \left\{ a \times b \,|\, ( a ; b) \in S
\right\} = \bigsqcap \mathrm{dom}\, S \times \bigsqcap \mathrm{im}\, S.$
And its corollary:
$latex ( a_0 \times b_0) \sqcap ( a_1 \times b_1) = ( a_0 \sqcap a_1) \times ( b_0
\sqcap b_1)$.
See this online article (here there is also the dual of the above statements).