let x be Real; :: thesis: ( x < 0 implies absreal . x = - x )
assume A1: 0 > x ; :: thesis: absreal . x = - x
absreal . x = |.x.| by EUCLID:def 2
.= - x by A1, ABSVALUE:def 1 ;
hence absreal . x = - x ; :: thesis: verum