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;

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;