:: deftheorem defines sqrt IDEAL_1:def 24 :
for R being non empty well-unital doubleLoopStr
for I being Subset of R holds sqrt I = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;