let a, b be real number ; :: thesis: ( 0 <= a & a <= b implies abs a <= abs b )
assume A1: ( 0 <= a & a <= b ) ; :: thesis: abs a <= abs b
then ( abs a = a & abs b = b ) by ABSVALUE:def 1;
hence abs a <= abs b by A1; :: thesis: verum