theorem :: SCMYCIEL:81

for G being SimpleGraph
for C being Coloring of (Complement G) holds C is Clique-partition of G