theorem :: XREAL_1:132

for a, b being Real st 0 < a & b < 0 holds
a * b < 0 ;