let R be symmetric RelStr ; :: thesis: for C being Clique-partition of R holds C is Coloring of (ComplRelStr R)
let C be Clique-partition of R; :: thesis: C is Coloring of (ComplRelStr R)
set CR = ComplRelStr R;
A: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def 9;

now

let x be set ; :: thesis: ( x in C implies x is StableSet of (ComplRelStr R) )
assume x in C ; :: thesis: x is StableSet of (ComplRelStr R)
then x is Clique of R by DILWORTH:def 11;
hence x is StableSet of (ComplRelStr R) by CliStaCompl; :: thesis: verum

end;

hence C is Coloring of (ComplRelStr R) by A, DILWORTH:def 12; :: thesis: verum