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