Description: Lemma for ismblfin ; could also be used to shorten proof of opnmbllem . (Contributed by Brendan Leahy, 13-Jul-2018)