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