theorem :: REALALG2:85

for R being preordered domRing
for P being Preordering of R
for a being square Element of R
for b1, b2 being Sqrt of a st 0. R <= P,b1 & 0. R <= P,b2 holds
b1 = b2 by sq0;