Round-six lemma `cBody_le`