Round-six lemma `Ut_le_X`