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

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

suppose r < 0 ; :: thesis: |.r.| = - r

hence |.r.| = - r by Def1; :: thesis: verum

end;

suppose r = 0 ; :: thesis: |.r.| = - r

hence |.r.| = - r by Th2; :: thesis: verum

end;

end;