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