theorem :: SCMYCIEL:83

for G being with_finite_cliquecover# SimpleGraph holds cliquecover# G = chromatic# (Complement G)