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