consider C being finite Clique-partition of R such that
A: card C = cliquecover# R by Lclico;
C is empty by EQREL_1:41;
hence cliquecover# R is empty by A; :: thesis: verum