Round-six lemma `c45_ok`