let p be quadratic Polynomial of R; :: thesis: not p is constant
deg p = 2 by defquadr;
hence not p is constant by RATFUNC1:def 2; :: thesis: verum