let a be real number ; :: thesis: ( a <= 0 implies sqrt (a ^2 ) = - a )
A1: a ^2 = (- a) ^2 ;
assume a <= 0 ; :: thesis: sqrt (a ^2 ) = - a
hence sqrt (a ^2 ) = - a by A1, Def4; :: thesis: verum