let G be SimpleGraph; :: thesis: for C being Coloring of (Complement G) holds C is Clique-partition of G
let C be Coloring of (Complement G); :: thesis: C is Clique-partition of G
Complement (Complement G) = G ;
hence C is Clique-partition of G by Th80; :: thesis: verum