New easy theorem and its consequence

I’ve added to my book a new easy to prove theorem and its corollary:

Theorem If $f$ is a (co-)complete funcoid then $\mathrm{up}\, f$ is a filter.

Corollary

1. If $f$ is a (co-)complete funcoid then $\mathrm{up}\, f = \mathrm{up} (\mathsf{RLD})_{\mathrm{out}} f$.
2. If $f$ is a (co-)complete reloid then $\mathrm{up}\, f = \mathrm{up}\, (\mathsf{FCD}) f$.