for R being transitive antisymmetric with_finite_clique# RelStr ex A being Coloring of R st card A = clique# R