Description: Define the class of all redundant sets x with respect to y in
z . For sets, binary relation on the class of all redundant sets
( brredunds ) is equivalent to satisfying the redundancy predicate
( df-redund ). (Contributed by Peter Mazsa, 23-Oct-2022)