:: deftheorem Def2 defines with_finite_chromatic# MYCIELSK:def 2 :
for R being RelStr holds
( R is with_finite_chromatic# iff ex C being Coloring of R st C is finite );