for R being non empty well-unital associative doubleLoopStr
for I being non empty Subset of R
for a being Element of R holds
( a in sqrt I iff ex n being Element of NAT st a |^ n in sqrt I )