let a, b, c be Real; :: thesis: ( a <= b & b <= c & not |.b.| <= |.a.| implies |.b.| <= |.c.| )
assume a1: ( a <= b & b <= c ) ; :: thesis: ( |.b.| <= |.a.| or |.b.| <= |.c.| )

per cases ( b >= 0 or b < 0 ) ;

suppose b >= 0 ; :: thesis: ( |.b.| <= |.a.| or |.b.| <= |.c.| )

then ( |.b.| = b & |.c.| = c ) by a1, ABSVALUE:def 1;
hence ( |.b.| <= |.a.| or |.b.| <= |.c.| ) by a1; :: thesis: verum

end;

suppose b < 0 ; :: thesis: ( |.b.| <= |.a.| or |.b.| <= |.c.| )

then ( |.a.| = - a & |.b.| = - b ) by a1, ABSVALUE:def 1;
hence ( |.b.| <= |.a.| or |.b.| <= |.c.| ) by a1, XREAL_1:24; :: thesis: verum

end;

end;