theorem Th31: :: MYCIELSK:31

for R being with_finite_chromatic# RelStr
for C being finite Coloring of R
for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )