:: deftheorem defines Squares_of REALALG1:def 10 :
for R being Ring holds Squares_of R = { a where a is Element of R : a is square } ;