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

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

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

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

end;

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

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

end;

end;