let a, b be Real; :: thesis: ( 0 <= a & a <= b implies |.a.| <= |.b.| )
assume that
A1: 0 <= a and
A2: a <= b ; :: thesis: |.a.| <= |.b.|
|.a.| = a by A1, ABSVALUE:def 1;
hence |.a.| <= |.b.| by A1, A2, ABSVALUE:def 1; :: thesis: verum