let a be real number ; :: thesis: ( a <= 0 implies sqrt (a ^2 ) = - a )
assume a <= 0 ; :: thesis: sqrt (a ^2 ) = - a
then ( - 0 <= - a & a ^2 = (- a) ^2 ) ;
hence sqrt (a ^2 ) = - a by Lm3; :: thesis: verum