theorem Th25: :: MYCIELSK:25

for R being RelStr
for C being Coloring of R holds C is Clique-partition of (ComplRelStr R)