theorem :: XREAL_1:34

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