It remains to show that there exists a finite coalgebra \(C\)  such
that \(\llbracket \phi  \rrbracket _{C} \ne \emptyset \) . This is immediate from the finite
model property of the coalgebraic \(\mu \) -calculus [1]};
alternatively, avoiding such overkill, it is seen as follows: We
define \(C=(X,\xi )\)  on the set \(X=\lbrace x_1,\dots ,x_k\rbrace \)  of the variables
in the above flat equation system by
\(\xi (x_i)\in \llbracket L_i \rrbracket _{X} (\lbrace x_1\rbrace ,\dots ,\lbrace x_k\rbrace )\)  where
\(\phi _i=L_i(x_1,\dots ,x_k)\) . Then by construction,
\((\lbrace x_1\rbrace ,\dots ,\lbrace x_k\rbrace )\)  is a fixed point of the equation system,
hence contained in the greatest fixed point, which proves the desired
non-emptiness of the greatest fixed point.
