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