Binary relations are essentially the same as pointfree funcoids between powersets

After this Math.StackExchange question I have proved that binary relations are essentially the same as pointfree funcoids between powersets.

Full proof is available in my draft book.

The most interesting aspect of this is that is that we can construct filtrator with core being pointfree funcoids from $latex \mathfrak{A}$ to $latex \mathfrak{B}$ for every poset of pointfree funcoids between filters on $latex \mathfrak{A}$ and filters on $latex \mathfrak{B}$, by analogy with the filtrator of funcoids whose core is a set of binary relations (the same as a pointfree funcoids, by the above bijective correspondence). This way the theory of filtrators of funcoids generalizes for pointfree funcoids.

By the way, this bijective correspondence is a functor.

Not understood? Read my book.