let x, y be Real; :: thesis: ( x * y < 0 implies ( 0 < x / (x - y) & x / (x - y) < 1 ) )
assume A1: x * y < 0 ; :: thesis: ( 0 < x / (x - y) & x / (x - y) < 1 )
then ( x <> 0 & y <> 0 ) ;

per cases then ( x < 0 or 0 < x ) ;

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

then y > 0 by A1;
then x - y < x by XREAL_1:44;
hence ( 0 < x / (x - y) & x / (x - y) < 1 ) by A2, XREAL_1:190; :: thesis: verum

end;

suppose A3: 0 < x ; :: thesis: ( 0 < x / (x - y) & x / (x - y) < 1 )

then y < 0 by A1;
then x < x - y by XREAL_1:46;
hence ( 0 < x / (x - y) & x / (x - y) < 1 ) by A3, XREAL_1:189; :: thesis: verum

end;

end;