take R = the empty RelStr ; :: thesis: R is with_finite_chromatic#
reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
take S ; :: according to MYCIELSK:def 2 :: thesis: S is finite
thus S is finite ; :: thesis: verum