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

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