Round-six lemma `c24_ok`