:: deftheorem Def5 defines cliquecover# MYCIELSK:def 5 :
for R being with_finite_cliquecover# RelStr
for b₂ being Nat holds
( b₂ = cliquecover# R iff ( ex C being finite Clique-partition of R st card C = b₂ & ( for C being finite Clique-partition of R holds b₂ <= card C ) ) );