Description: Inference from Theorem 19.21 of Margaris p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999) Shortened after introduction of hbralrimi . (Revised by Wolf Lammen, 4-Dec-2019)