About “Each regular paratopological group is completely regular” article

In this blog post I consider my attempt to rewrite the article “Each regular paratopological group is completely regular” by Taras Banakh, Alex Ravsky in a more abstract way using my theory of reloids and funcoids.

The following is a general comment about reloids and funcoids as defined in my book. If you don’t understand them, restrict your mind to the special case $latex {f}&fg=000000$ to be a quasi-uniform space and $latex {(\mathsf{FCD}) f}&fg=000000$ is the corresponding quasi-proximity.

$latex {\langle f \rangle^{\ast}}&fg=000000$ is the closure operator corresponding to a funcoid $latex {f}&fg=000000$. I also denote the image $latex {\mathscr{P} X \rightarrow \mathscr{P} Y}&fg=000000$ of a function $latex {f : X \rightarrow Y}&fg=000000$ as $latex {\langle f \rangle^{\ast}}&fg=000000$.

I will also denote $latex {f^{\circ}}&fg=000000$ the interior funcoid for a co-complete funcoid $latex {f}&fg=000000$ (for the special case if $latex {f}&fg=000000$ is a topological space $latex {f^{\circ}}&fg=000000$ is the interior operator of this space). It is defined in the file addons.pdf (not yet in my book).

By definition (slightly generalizing the special case if $latex {f}&fg=000000$ is a quasi-uniform space) an endo-reloid $latex {f}&fg=000000$ on a set $latex {U}&fg=000000$ is normal when $latex {\langle (\mathsf{FCD}) f \rangle^{\ast} A \sqsubseteq \langle ((\mathsf{FCD}) f)^{\circ} \rangle^{\ast} \langle (\mathsf{FCD}) f \rangle^{\ast} \langle F \rangle^{\ast} A}&fg=000000$ for every entourage $latex {F \in \mathrm{up}\, f}&fg=000000$ of $latex {f}&fg=000000$ and every set $latex {A \subseteq U}&fg=000000$.

Then it appear “obvious” that this definition of normality is equivalent to the formula:

$latex \displaystyle (\mathsf{FCD}) f \sqsubseteq ((\mathsf{FCD}) f)^{\circ} \circ (\mathsf{FCD}) f \circ (\mathsf{FCD}) f. &fg=000000$

However, I have failed to prove it. Here is my attempt

$latex \langle ((\mathsf{FCD}) f)^{\circ} \rangle^{\ast} \langle (\mathsf{FCD}) f \rangle^{\ast} \langle (\mathsf{FCD}) f \rangle^{\ast} A = \\ \langle ((\mathsf{FCD}) f)^{\circ} \rangle^{\ast} \langle (\mathsf{FCD}) f \rangle^{\ast} \bigsqcap_{F \in \mathrm{up} f} \langle F \rangle^{\ast} A = \\ \langle ((\mathsf{FCD}) f)^{\circ} \rangle^{\ast} \bigsqcap_{F \in \mathrm{up} f} \langle (\mathsf{FCD}) f \rangle^{\ast} \langle F \rangle^{\ast} A = ? ?&fg=000000$

The further step fails because in general $latex {\langle ((\mathsf{FCD}) f)^{\circ} \rangle^{\ast} \bigsqcap_{F \in \mathrm{up} f} S \neq \bigsqcap_{F \in \mathrm{up} f} \langle \langle ((\mathsf{FCD}) f)^{\circ} \rangle^{\ast} \rangle^{\ast} S}&fg=000000$.

So as now my attempt has failed. Please give me advice how to overcome this shortcoming of my theory.