§7, p. 218 — C_𝒢(L), F_𝒢(L) (and C_𝒢(L) ∩ F_𝒢(L)) contain their supremal elements

Let $\mathcal G$ be a generator over a finite alphabet with controllable events $\Sigma_c$ and $L(\mathcal G) = \bar L_m(\mathcal G)$, and let $L \subseteq L(\mathcal G)$. Each of the classes

contains a (necessarily unique) greatest element with respect to inclusion, namely the union of all its members; these are denoted $\sup \mathbf C_{\mathcal G}(L)$, $\sup \mathbf F_{\mathcal G}(L)$ and $\sup\{\mathbf C_{\mathcal G}(L) \cap \mathbf F_{\mathcal G}(L)\}$.

The supremal controllable sublanguage is the central object of the theory: Theorem 7.1 identifies it as the behaviour of the minimally restrictive supervisor.

Formalization Note. $\sup$ is sSup in the complete lattice Set (List α) (the union of the class), and "contains its supremal element" is IsGreatest. The third class is the one Theorem 7.1 (ii) uses; the paper covers it by "In fact, $\mathbf C_{\mathcal G}(L)$ and $\mathbf F_{\mathcal G}(L)$ are complete subsemilattices".