theorem Th80: :: SCMYCIEL:80

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