let p be quadratic Element of the carrier of (Polynom-Ring R); :: thesis: not p is constant
deg p = 2 by defquadr;
hence not p is constant by RING_4:def 4; :: thesis: verum