:: deftheorem defines with_sums_of_squares REALALG1:def 13 :
for R being Ring
for S being Subset of R holds
( S is with_sums_of_squares iff QS R c= S );