Description: Lemma 1 for eleclclwwlkn . (Contributed by Alexander van der Vekens, 11-May-2018) (Revised by AV, 30-Apr-2021)