let r be Real; :: thesis: ( r <= 0 implies abs r = - r )
assume A1: r <= 0 ; :: thesis: abs r = - r

per cases ( r < 0 or r = 0 ) by A1;

suppose r < 0 ; :: thesis: abs r = - r

hence abs r = - r by ABSVALUE:def 1; :: thesis: verum

end;

suppose r = 0 ; :: thesis: abs r = - r

hence abs r = - r by ABSVALUE:7; :: thesis: verum

end;

end;