:: deftheorem defines with_squares REALALG1:def 12 :
for R being Ring
for S being Subset of R holds
( S is with_squares iff SQ R c= S );