theorem :: XREAL_1:27

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