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

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

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

hence ( 0 < y & |.x.| < y ) by A1, EXTREAL1:def 3; :: thesis: verum

end;

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

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

end;

end;