One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) Remove dependencies on [ax-5], [ax-6], [ax-7], [ax-10], [ax-12]. (Revised by Wolf Lammen, 8-Jan-2018.)
One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) Remove dependencies on [ax-5], [ax-6], [ax-7], [ax-10], [ax-12]. (Revised by Wolf Lammen, 8-Jan-2018.)