let x, y be R_eal; :: thesis: ( ( ( x = +infty & y < 0 & -infty < y ) or ( x = -infty & 0 < y & y < +infty ) ) implies x / y = -infty )
assume A1: ( ( x = +infty & y < 0 & -infty < y ) or ( x = -infty & 0 < y & y < +infty ) ) ; :: thesis: x / y = -infty

per cases ( ( x = +infty & y < 0 & -infty < y ) or ( x = -infty & 0 < y & y < +infty ) ) by A1;

suppose ( x = +infty & y < 0 & -infty < y ) ; :: thesis: x / y = -infty

hence x / y = -infty by EXTREAL1:def 2; :: thesis: verum

end;

suppose ( x = -infty & 0 < y & y < +infty ) ; :: thesis: x / y = -infty

hence x / y = -infty by EXTREAL1:def 2; :: thesis: verum

end;

end;