let y be ExtReal; :: 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, Th82;
hence +infty / y = +infty by A1, Def5; :: thesis: verum