let x, y be ExtReal; :: thesis: ( y <> -infty & 0 < x & y < 0 implies x / y < 0 )
assume that
A1: y <> -infty and
A2: 0 < x and
A3: y < 0 ; :: thesis: x / y < 0
reconsider y1 = y as Element of REAL by A1, A3, XXREAL_0:14;

per cases ( x in REAL or x = +infty or x = -infty ) by XXREAL_0:14;

suppose x in REAL ; :: thesis: x / y < 0

then reconsider x1 = x as Real ;
x / y = x1 / y1 by EXTREAL1:2;
hence x / y < 0 by A2, A3; :: thesis: verum

end;

suppose x = +infty ; :: thesis: x / y < 0

hence x / y < 0 by A1, A3, XXREAL_3:85; :: thesis: verum

end;

suppose x = -infty ; :: thesis: x / y < 0

hence x / y < 0 by A2; :: thesis: verum

end;

end;