let r be real number ; :: 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 Def1; :: thesis: verum

end;

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

hence abs r = - r by Th2; :: thesis: verum

end;

end;