# A new theorem proved

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

It was easy to show:

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

Today I’ve proved the following important theorem:

Theorem If $S$ is a filter base on the set of funcoids then $S$ is a base of $\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.