let x be R_eal; :: thesis: ( - |.x.| <= x & x <= |.x.| )

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

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

0 <= |.x.| by Th51;
hence ( - |.x.| <= x & x <= |.x.| ) by A1, EXTREAL1:24, EXTREAL1:def 3, SUPINF_2:16; :: thesis: verum

end;

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

then |.x.| = - x by EXTREAL1:def 3;
hence ( - |.x.| <= x & x <= |.x.| ) by A2, EXTREAL1:25; :: thesis: verum

end;

end;