set a = the non square Element of F;
reconsider p = <%(- the non square Element of F),(0. F),(1. F)%> as quadratic Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
take p ; :: thesis: ( p is monic & not p is DC-square )
A: DC p = - (4 '*' (- the non square Element of F)) by defDCpq
.= - (- (4 '*' the non square Element of F)) by REALALG2:6 ;
H: ( 2 '*' (1. F) <> 0. F & 4 '*' (1. F) <> 0. F ) by ch2, ch4;

now :: thesis: not p is DC-square

assume p is DC-square ; :: thesis: contradiction
then consider w being Element of F such that
C: w ^2 = 4 '*' the non square Element of F by A, O_RING_1:def 2;
w * w = 4 '*' ((1. F) * the non square Element of F) by C, O_RING_1:def 1
.= (4 '*' (1. F)) * the non square Element of F by REALALG2:5
.= the non square Element of F * (4 '*' (1. F)) by GROUP_1:def 12 ;
then (w * w) * ((4 '*' (1. F)) ") = the non square Element of F * ((4 '*' (1. F)) * ((4 '*' (1. F)) ")) by GROUP_1:def 3
.= the non square Element of F * (((4 '*' (1. F)) ") * (4 '*' (1. F))) by GROUP_1:def 12
.= the non square Element of F * (1. F) by H, VECTSP_1:def 10 ;
then the non square Element of F = (w * w) * (((2 * 2) '*' (1. F)) ")
.= (w * w) * (((2 '*' (1. F)) * (2 '*' (1. F))) ") by RING_3:67
.= (w * w) * (((2 '*' (1. F)) ") * ((2 '*' (1. F)) ")) by H, VECTSP_2:11
.= w * (w * (((2 '*' (1. F)) ") * ((2 '*' (1. F)) "))) by GROUP_1:def 3
.= w * ((w * ((2 '*' (1. F)) ")) * ((2 '*' (1. F)) ")) by GROUP_1:def 3
.= w * (((2 '*' (1. F)) ") * (w * ((2 '*' (1. F)) "))) by GROUP_1:def 12
.= (w * ((2 '*' (1. F)) ")) * (w * ((2 '*' (1. F)) ")) by GROUP_1:def 3
.= (w * ((2 '*' (1. F)) ")) ^2 by O_RING_1:def 1 ;
hence contradiction ; :: thesis: verum

end;

hence ( p is monic & not p is DC-square ) ; :: thesis: verum