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;
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 (ComplRelStr R)

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 Th19; :: thesis: verum

end;

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