theorem :: XREAL_1:33

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