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