Description: Two classes are related by the membership relation if and only if they are
related by the membership relation (i.e., the first is an element of the
second) and the second is a set (hence so is the first). TODO: move to
Main after reordering to have brrelex2i available. Check if it is
shorter to prove bj-epelg first or bj-epelb first. (Contributed by BJ, 14-Jul-2023)