theorem :: SQUARE_1:23

for a being Real st a <= 0 holds
sqrt (a ^2) = - a