for x being R_eal st x < 0 holds
|.x.| = - x by Def1;