:: deftheorem Def17 defines with_finite_cliquecover# SCMYCIEL:def 17 :
for G being SimpleGraph holds
( G is with_finite_cliquecover# iff ex C being Clique-partition of G st C is finite );