let R be symmetric RelStr ; :: thesis: for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R
let C be Clique-partition of (ComplRelStr R); :: thesis: C is Coloring 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 StableSet of R

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

end;

hence C is Coloring of R by A1, DILWORTH:def 12; :: thesis: verum