Round-six lemma `g15_ok`