let R be finite RelStr ; :: thesis: cliquecover# R <= card the carrier of R
consider C being finite Clique-partition of R such that
A1: card C = cliquecover# R by Def5;
card C c= card the carrier of R by Th7;
hence cliquecover# R <= card the carrier of R by A1, NAT_1:39; :: thesis: verum