let F be formally_real Field; :: thesis: not F is algebraic-closed
set P = the Ordering of F;
set p = npoly (F,2);
D: deg (npoly (F,2)) = 2 by RING_5:43;
A: (deg (npoly (F,2))) + 1 = ((len (npoly (F,2))) - 1) + 1 by HURWITZ:def 2;
now :: thesis: not F is algebraic-closed
assume F is algebraic-closed ; :: thesis: contradiction
then consider a being Element of F such that
B: a is_a_root_of npoly (F,2) by A, D, POLYNOM5:def 9, POLYNOM5:def 8;
0. F = eval ((npoly (F,2)),a) by B, POLYNOM5:def 7
.= (a |^ 2) - (- (1. F)) by RING_5:46 ;
then - (1. F) = a |^ 2 by RLVECT_1:21
.= a ^2 by RING_5:3 ;
then - (1. F) in QS F ;
hence contradiction by REALALG1:26; :: thesis: verum
end;
hence not F is algebraic-closed ; :: thesis: verum