:: deftheorem defines Quadratic_Sums_of REALALG1:def 11 :
for R being Ring holds Quadratic_Sums_of R = { a where a is Element of R : a is sum_of_squares } ;