Description: Lemma for unxpdom . (Contributed by Mario Carneiro, 13-Jan-2013) (Revised by Mario Carneiro, 16-Nov-2014)