let x, y be ExtReal; :: thesis: ( ( - y <= x & x <= y ) iff |.x.| <= y )
A1: ( - y <= x & x <= y implies |.x.| <= y )

proof

assume that
A2: - y <= x and
A3: x <= y ; :: thesis: |.x.| <= y

per cases ( 0 <= x or not 0 <= x ) ;

suppose 0 <= x ; :: thesis: |.x.| <= y

hence |.x.| <= y by A3, Def1; :: thesis: verum

end;

suppose A4: not 0 <= x ; :: thesis: |.x.| <= y

- x <= y by A2, XXREAL_3:60;
hence |.x.| <= y by A4, Def1; :: thesis: verum

end;

end;

end;

( |.x.| <= y implies ( - y <= x & x <= y ) )

proof

assume A5: |.x.| <= y ; :: thesis: ( - y <= x & x <= y )

per cases ( |.x.| = y or |.x.| < y ) by A5, XXREAL_0:1;

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

hence ( - y <= x & x <= y ) by Th9; :: thesis: verum

end;

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

hence ( - y <= x & x <= y ) by Th10; :: thesis: verum

end;

end;

end;

hence ( ( - y <= x & x <= y ) iff |.x.| <= y ) by A1; :: thesis: verum