theorem :: XREAL_1:195

for a, b being Real st b <= 0 & a <= - b holds
- 1 <= a / b