let G be with_finite_cliquecover# SimpleGraph; :: thesis: cliquecover# G = chromatic# (Complement G)
Complement (Complement G) = G ;
hence cliquecover# G = chromatic# (Complement G) by Th82; :: thesis: verum