let R be non degenerated Ring; :: thesis: ( R is algebraic-closed implies R is quadratic_complete )
assume AS: R is algebraic-closed ; :: thesis: R is quadratic_complete

now :: thesis: for o being object st o in the carrier of R holds
o in SQ R

let o be object ; :: thesis: ( o in the carrier of R implies o in SQ R )
assume o in the carrier of R ; :: thesis: o in SQ R
then reconsider a = o as Element of R ;
set p = X^2- a;
2 = deg (X^2- a) by qua4
.= (len (X^2- a)) - 1 by HURWITZ:def 2 ;
then len (X^2- a) = 3 ;
then consider b being Element of R such that
A: b is_a_root_of X^2- a by AS, POLYNOM5:def 8;
0. R = ((- a) + ((0. R) * b)) + ((1. R) * (b ^2)) by A, evalq
.= (b ^2) - a ;
then b ^2 = - (- a) by RLVECT_1:6;
then a in { x where x is Element of R : x is square } ;
hence o in SQ R by REALALG1:def 10; :: thesis: verum

end;

hence R is quadratic_complete by TARSKI:def 3; :: thesis: verum