:: deftheorem defqc defines quadratic_complete FIELD_9:def 20 :
for R being Ring holds
( R is quadratic_complete iff the carrier of R c= SQ R );