theorem :: XREAL_1:130

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