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