theorem :: REALALG2:86

for R being ordered domRing
for O being Ordering of R
for a being square Element of R
for b being Element of R holds
( b is Sqrt of a iff ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) )