theorem :: XREAL_1:28

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