let x, y be ExtReal; :: thesis: ( |.x.| < y implies ( - y < x & x < y ) )
assume A1: |.x.| < y ; :: thesis: ( - y < x & x < y )
reconsider x = x, y = y as R_eal by XXREAL_0:def 1;
A2: |.x.| < y by A1;

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

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

hence ( - y < x & x < y ) by A2, Def1; :: thesis: verum

end;

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

then |.x.| = - x by Def1;
hence ( - y < x & x < y ) by A1, A3, XXREAL_3:60; :: thesis: verum

end;

end;