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;