let R be Ring; :: thesis: ( not R is quadratic_complete implies not R is degenerated )
assume A: not R is quadratic_complete ; :: thesis: not R is degenerated

now :: thesis: not R is degenerated

assume B: R is degenerated ; :: thesis: contradiction

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 ;
a = a * (1. R)
.= 0. R by B ;
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;

then the carrier of R c= SQ R ;
hence contradiction by A; :: thesis: verum

end;

hence not R is degenerated ; :: thesis: verum