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