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