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