Description: Restricted quantifier version of 19.30 . (Contributed by Scott Fenton, 25-Feb-2011) (Proof shortened by Wolf Lammen, 18-Jun-2023)