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