Round-six lemma `isPiv_mid`