Round-six lemma `g24_ok`