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