ACM Computing Classification System (1998): G.1.1, G.1.2.We consider optimal Lagrange interpolation with polynomials of degree at most two on the unit interval [−1, 1]. In a largely unknown paper, Schurer (1974, Stud. Sci. Math. Hung. 9, 77-79) has analytically described the infinitely many zero-symmetric and zero-asymmetric extremal node systems −1 ≤ x1 < x2 < x3 ≤ 1 which all lead to the minimal Lebesgue constant 1.25 that had already been determined by Bernstein (1931, Izv. Akad. Nauk SSSR 7, 1025-1050). As Schurer’s proof is not given in full detail, we formally verify it by providing two new and sound proofs of his theorem with the aid of symbolic computation using quantifier elimination. Additionally, we provide an alternative, but eq...