:: deftheorem Def18 defines cliquecover# SCMYCIEL:def 18 :
for G being with_finite_cliquecover# SimpleGraph
for b₂ being Nat holds
( b₂ = cliquecover# G iff ( ex C being finite Clique-partition of G st card C = b₂ & ( for C being finite Clique-partition of G holds b₂ <= card C ) ) );