:: deftheorem defsqrt defines SquareRoot REALALG2:def 12 :
for R being Ring
for a being square Element of R
for b₃ being Element of R holds
( b₃ is SquareRoot of a iff b₃ ^2 = a );