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