Deduction form of Theorem 19.20 of [Margaris] p. 90 with two quantifiers, see alim. (Contributed by NM, 27-Apr-2004.)