:: deftheorem defq defines sqrt REALALG2:def 13 :
for R being ordered domRing
for O being Ordering of R
for a being square Element of R
for b₄ being non b₂ -negative Sqrt of a holds
( b₄ = sqrt (O,a) iff b₄ ^2 = a );