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