|.(- a).| = - (- a) by ABSVALUE:30;
hence |.(- a).| = a ; :: thesis: verum