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

now :: thesis: for x being set st x in C holds
x is StableSet of G

let x be set ; :: thesis: ( x in C implies x is StableSet of G )
assume A1: x in C ; :: thesis: x is StableSet of G
then A2: (Complement G) SubgraphInducedBy x is Clique of (Complement G) by Def16;
union ((Complement G) SubgraphInducedBy x) = x by A1, Lm9;
hence x is StableSet of G by A2, Th73; :: thesis: verum

end;

hence C is Coloring of G by Lm4, Def20; :: thesis: verum