:: deftheorem defines being_a_square O_RING_1:def 2 :
for R being non empty doubleLoopStr
for x being Scalar of R holds
( x is being_a_square iff ex y being Scalar of R st x = y ^2 );