:: deftheorem Def4 defines with_finite_cliquecover# MYCIELSK:def 4 :
for R being RelStr holds
( R is with_finite_cliquecover# iff ex C being Clique-partition of R st C is finite );