let x be ExtReal; :: thesis: ( - |.x.| <= x & x <= |.x.| )
reconsider x = x as R_eal by XXREAL_0:def 1;

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

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

thus ( - |.x.| <= x & x <= |.x.| ) by A1, Def1; :: thesis: verum

end;

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

then |.x.| = - x by Def1;
hence ( - |.x.| <= x & x <= |.x.| ) ; :: thesis: verum

end;

end;