theorem :: XREAL_1:128

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