set q = npoly (F_Real,2);
A: 0 + 2 is even ;
now :: thesis: not F_Real is algebraic-closed
assume AS: F_Real is algebraic-closed ; :: thesis: contradiction
(len (npoly (F_Real,2))) - 1 = deg (npoly (F_Real,2)) by HURWITZ:def 2
.= 2 by lem6 ;
then len (npoly (F_Real,2)) = 3 ;
hence contradiction by A, AS, POLYNOM5:def 9; :: thesis: verum
end;
hence not F_Real is algebraic-closed ; :: thesis: verum