let a, x be Real; :: thesis: ( 0 <= a implies ( ( x <= - a or a <= x ) iff a <= |.x.| ) )
assume AS: 0 <= a ; :: thesis: ( ( x <= - a or a <= x ) iff a <= |.x.| )

hereby :: thesis: ( not a <= |.x.| or x <= - a or a <= x )

assume A1: ( x <= - a or a <= x ) ; :: thesis: a <= |.x.|

per cases ( a = x or - a = x or ( not a = x & not - a = x ) ) ;

suppose ( a = x or - a = x ) ; :: thesis: a <= |.x.|

then |.a.| = |.x.| by COMPLEX1:52;
hence a <= |.x.| by AS, ABSVALUE:def 1; :: thesis: verum

end;

suppose ( not a = x & not - a = x ) ; :: thesis: a <= |.x.|

then ( x < - a or a < x ) by A1, XXREAL_0:1;
hence a <= |.x.| by ABSVALUE:5; :: thesis: verum

end;

end;

end;

assume A0: a <= |.x.| ; :: thesis: ( x <= - a or a <= x )

per cases ( a = |.x.| or a <> |.x.| ) ;

suppose a = |.x.| ; :: thesis: ( x <= - a or a <= x )

then ( a = x or a = - x ) by ABSVALUE:1;
hence ( x <= - a or a <= x ) ; :: thesis: verum

end;

suppose a <> |.x.| ; :: thesis: ( x <= - a or a <= x )

then a < |.x.| by A0, XXREAL_0:1;
hence ( x <= - a or a <= x ) by ABSVALUE:5; :: thesis: verum

end;

end;