set q = npoly (F_Real,2);

A: 0 + 2 is even ;

A: 0 + 2 is even ;

now :: thesis: not F_Real is algebraic-closed

hence
not F_Real is algebraic-closed
; :: thesis: verumassume 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;(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