let R be RelStr ; :: thesis: ( R is finite implies R is with_finite_cliquecover# )
set cR = the carrier of R;
assume A1: R is finite ; :: thesis: R is with_finite_cliquecover#

per cases ( R is empty or not R is empty ) ;

suppose R is empty ; :: thesis: R is with_finite_cliquecover#

then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
for x being set st x in S holds
x is Clique of R ;
then reconsider S = S as Clique-partition of R by DILWORTH:def 11;
take S ; :: according to MYCIELSK:def 4 :: thesis: S is finite
thus S is finite ; :: thesis: verum

end;

suppose A2: not R is empty ; :: thesis: R is with_finite_cliquecover#

reconsider cRp1 = the carrier of R as non empty finite set by A2, A1;
set S = SmallestPartition the carrier of R;
deffunc H₁( set ) -> set = {c₁};
A3: SmallestPartition the carrier of R = { H₁(x) where x is Element of cRp1 : S₁[x] } by EQREL_1:37;
A4: { H₁(x) where x is Element of cRp1 : S₁[x] } is finite from PRE_CIRC:sch 1();

now :: thesis: for z being set st z in SmallestPartition the carrier of R holds
z is Clique of R

let z be set ; :: thesis: ( z in SmallestPartition the carrier of R implies z is Clique of R )
assume A5: z in SmallestPartition the carrier of R ; :: thesis: z is Clique of R
ex x being Element of the carrier of R st z = {x} by A5, A3;
hence z is Clique of R by A2, SUBSET_1:33; :: thesis: verum

end;

then reconsider S = SmallestPartition the carrier of R as Clique-partition of R by DILWORTH:def 11;
take S ; :: according to MYCIELSK:def 4 :: thesis: S is finite
thus S is finite by A4; :: thesis: verum

end;

end;