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 A0: x in C ; :: thesis: x is StableSet of G
then A1: (Complement G) SubgraphInducedBy x is Clique of (Complement G) by LCliquewise;
union ((Complement G) SubgraphInducedBy x) = x by A0, Sub0c;
hence x is StableSet of G by A1, CliComplSta; :: thesis: verum

end;

hence C is Coloring of G by Compl1, LStableSetwise; :: thesis: verum