let x, y be R_eal; :: thesis: ( |.x.| < y implies ( - y < x & x < y ) )
assume A1: |.x.| < y ; :: thesis: ( - y < x & x < y )

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

suppose A2: 0 <= x ; :: thesis: ( - y < x & x < y )

then x < y by A1, EXTREAL1:def 3;
hence ( - y < x & x < y ) by A2; :: thesis: verum

end;

suppose A3: not 0 <= x ; :: thesis: ( - y < x & x < y )

then |.x.| = - x by EXTREAL1:def 3;
hence ( - y < x & x < y ) by A1, A3, XXREAL_3:71; :: thesis: verum

end;

end;