let G be SimpleGraph; :: thesis: for C being Coloring of G holds C is Clique-partition of (Complement G)
let C be Coloring of G; :: thesis: C is Clique-partition of (Complement G)
set CG = Complement G;

now :: thesis: for x being set st x in C holds
(Complement G) SubgraphInducedBy x is Clique of (Complement G)

let x be set ; :: thesis: ( x in C implies (Complement G) SubgraphInducedBy x is Clique of (Complement G) )
assume x in C ; :: thesis: (Complement G) SubgraphInducedBy x is Clique of (Complement G)
then x is StableSet of G by Def20;
hence (Complement G) SubgraphInducedBy x is Clique of (Complement G) by Th74; :: thesis: verum

end;

hence C is Clique-partition of (Complement G) by Lm4, Def16; :: thesis: verum