I’ve added to my book a new easy to prove theorem and its corollary:
Theorem If $latex f$ is a (co-)complete funcoid then $latex \mathrm{up}\, f$ is a filter.
Corollary
- If $latex f$ is a (co-)complete funcoid then $latex \mathrm{up}\, f = \mathrm{up} (\mathsf{RLD})_{\mathrm{out}} f$.
- If $latex f$ is a (co-)complete reloid then $latex \mathrm{up}\, f = \mathrm{up}\, (\mathsf{FCD}) f$.