**Definition** A set $latex S$ of binary relations is a *base* of a funcoid $latex f$ when all elements of $latex S$ are above $latex f$ and $latex \forall X \in \mathrm{up}\, f \exists T \in S : T \sqsubseteq X$.

It was easy to show:

**Proposition** A set $latex S$ of binary relations is a base of a funcoid iff it is a base of $latex \bigsqcap^{\mathsf{FCD}} S$.

Today I’ve proved the following important theorem:

**Theorem** If $latex S$ is a filter base on the set of funcoids then $latex S$ is a base of $latex \bigsqcap^{\mathsf{FCD}} S$.

The proof is currently located in this PDF file.

It is yet unknown whether the converse theorem holds, that is whether every base of a funcoid is a filter base on the set of funcoids.

## 1 thought on “A new theorem proved”