let R be RelStr ; :: thesis: for C being Coloring of (ComplRelStr R) holds C is Clique-partition of R
let C be Coloring of (ComplRelStr R); :: thesis: C is Clique-partition of R
set CR = ComplRelStr R;
A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def 8;
now :: thesis: for x being set st x in C holds
x is Clique of R
let x be set ; :: thesis: ( x in C implies x is Clique of R )
assume x in C ; :: thesis: x is Clique of R
then x is StableSet of (ComplRelStr R) by DILWORTH:def 12;
hence x is Clique of R by Th22; :: thesis: verum
end;
hence C is Clique-partition of R by A1, DILWORTH:def 11; :: thesis: verum