theorem :: MYCIELSK:16

for R being with_finite_stability# with_finite_cliquecover# RelStr holds stability# R <= cliquecover# R