consider a being non zero Element of R, b, c being Element of R such that
H: p = <%c,b,a%> by qua5;
(b ^2) - ((4 '*' a) * c) is Element of R ;
hence ex b₁ being Element of R ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b₁ = (b ^2) - ((4 '*' a) * c) ) by H; :: thesis: verum