theorem Th47: :: MYCIELSK:47

for R being with_finite_chromatic# RelStr
for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S)