Description: Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 . (Contributed by AV, 29-Jan-2021) (Revised by AV, 18-Sep-2021)