let r be Real; :: thesis: ( r <= 0 implies |.r.| = - r )
assume r <= 0 ; :: thesis: |.r.| = - r
then ( r < 0 or r = 0 ) ;
hence |.r.| = - r by Def1; :: thesis: verum