Description: "At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023)