let x, y be ExtReal; :: thesis: ( - y < x & x < y implies ( 0 < y & |.x.| < y ) )
assume that
A1: - y < x and
A2: 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 A2, Def1; :: thesis: verum

end;

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

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

end;

end;