theorem :: XREAL_1:126

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