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

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

end;

hence C is Clique-partition of (ComplRelStr R) by A1, DILWORTH:def 11; :: thesis: verum