Round-six lemma `setCost_le`