theorem Th27: :: MYCIELSK:27

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