Monovalued reloids are metamonovalued

I’ve proved today the theorem:

Theorem Monovalued reloids are metamonovalued.

In other words:

Theorem $latex \left( \bigsqcap G \right) \circ f = \bigsqcap \left\{ g \circ f \,|\, g \in G \right\}$ if $latex f$ is a monovalued reloid and $latex G$ is a set of reloids (with matching sources and destination).

The proof uses the lemma, which is a special case (when $latex f$ is a principal reloid) of the theorem. The proof is now presented in the preprint of my book.