:: deftheorem Def2 defines sqrt SQUARE_1:def 2 :
for a being Real st 0 <= a holds
for b₂ being Real holds
( b₂ = sqrt a iff ( 0 <= b₂ & b₂ ^2 = a ) );