theorem :: XREAL_1:29

for a, b being Real st 0 < a holds
b < b + a by Lm9;