let x, y be ExtReal; :: thesis: ( y <> +infty & x < 0 & 0 < y implies x / y < 0 )
assume that
A1: y <> +infty and
A2: x < 0 and
A3: 0 < y ; :: thesis: x / y < 0
reconsider y1 = y as Element of REAL by A3, A1, 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 A2; :: thesis: verum

end;

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

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

end;

end;