let a be Real; :: 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, Def2; :: thesis: verum