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