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