theorem Th15: :: MYCIELSK:15
for R being with_finite_clique# with_finite_chromatic# RelStr holds clique# R <= chromatic# R