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.| )

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 A0:
a <= |.x.|
; :: thesis: ( x <= - a or a <= x )assume A1:
( x <= - a or a <= x )
; :: thesis: a <= |.x.|

end;