theorem :: SQUARE_1:22

for a being Real st 0 <= a holds
sqrt (a ^2) = a by Def2;