Normality of a quasi-uniform space on a topology is determined by the proximity induced by the quasi-uniform space

First a prelude:

Taras Banakh, Alex Ravsky “Each regular paratopological group is completely regular” solved a 60 year old open problem.

Taras Banakh introduces what he call normal uniformities (don’t confuse with normal topologies).

My new result, proved with advanced funcoids theory (and never tried to prove it with basic general topology): Whether a uniformity on a topology is normal is determined by the proximity induced by the uniformity. (Moreover I expressed it as an explicit algebraic formula in terms of funcoids: $latex \nu\circ\nu^{-1}\sqsubseteq\nu^{-1}\circ\mu$, where $latex \mu$ is the proximity induced by the quasi-uniformity and $latex \nu$ is the topological space).