let y be ext-real number ; :: thesis: ( 0 < y & y <> +infty implies +infty / y = +infty )
assume that
A1: 0 < y and
A2: y <> +infty ; :: thesis: +infty / y = +infty
y " <> 0 by A1, A2, Th93;
hence +infty / y = +infty by A1, Def5; :: thesis: verum