theorem Th1: :: TOPREAL6:2

for a, b being Real st 0 <= a & a <= b holds
|.a.| <= |.b.|